projects / coq-categories.git / search
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
add Notations.v
2011-04-06 Adam Megaczadd Notations.v
 commit | commitdiff | tree
2011-04-06 Adam Megaczremove reliance on General.v
 commit | commitdiff | tree
2011-04-06 Adam Megaczmake the Functor of {Pre}MonoidalFunctor a parameter...
commit | commitdiff | tree
2011-04-05 Adam MegaczPreMonoidalCategories: remove the very last [[admit]]
 commit | commitdiff | tree
2011-04-05 Adam Megaczadd special case of ni_respects where one side is exactly...
commit | commitdiff | tree
2011-04-05 Adam Megaczrename Retraction to RetractionOfCategories
 commit | commitdiff | tree
2011-04-05 Adam Megaczformatting fixes
 commit | commitdiff | tree
2011-04-05 Adam Megaczremove Arrows.v
 commit | commitdiff | tree
2011-04-05 Adam Megaczfix miscompilation errors introduced by recent changes
 commit | commitdiff | tree
2011-04-05 Adam Megaczflip around the pentagon to the opposite of Mac Lane...
commit | commitdiff | tree
2011-04-05 Adam Megaczadd proof of MacLane_ex_VII_1_1
 commit | commitdiff | tree
2011-04-04 Adam Megaczmajor revision: separate Subcategory into {Wide,Full...
commit | commitdiff | tree
2011-04-03 Adam Megaczmajor revision: MonoidalCat is now a subclass of PreMonoidalCat
 commit | commitdiff | tree
2011-04-03 Adam MegaczMakefile: insist on native-compiled Coq
 commit | commitdiff | tree
2011-04-03 Adam Megaczadd README
 commit | commitdiff | tree
2011-04-02 Adam Megaczsplit MonoidalCategories into Binoidal and PreMonoidal
 commit | commitdiff | tree
2011-04-02 Adam Megaczadd isos_forward_equal_then_backward_equal, iso_inv_inv
 commit | commitdiff | tree
2011-03-29 Adam Megaczfinish the proof of ffc_functor_weakly_monic
 commit | commitdiff | tree
2011-03-29 Adam Megaczfurther work on CenterMonoidal
 commit | commitdiff | tree
2011-03-29 Adam Megaczcomment out unused portion of RepresentableStructure_ch7_2
 commit | commitdiff | tree
2011-03-29 Adam Megaczrename RepresentableFunctor to HomFunctor
 commit | commitdiff | tree
2011-03-28 Adam Megaczmake mf_compose_coherence transparent
 commit | commitdiff | tree
2011-03-27 Adam MegaczIsomorphicCategories: make the components fields, not...
commit | commitdiff | tree
2011-03-27 Adam Megaczadd SurjectiveEnrichment to SMME
 commit | commitdiff | tree
2011-03-27 Adam Megaczpartial implementation of MonoidalFunctorsCompose
 commit | commitdiff | tree
2011-03-26 Adam Megaczfix typo
 commit | commitdiff | tree
2011-03-26 Adam Megaczadd Retraction, SMME, make Enrichment a parameter
 commit | commitdiff | tree
2011-03-25 Adam Megaczadd func_diagonal, fix naturality for DiagonalCat
 commit | commitdiff | tree
2011-03-25 Adam Megaczfix Freyd Categories
 commit | commitdiff | tree
2011-03-25 Adam Megaczfix naturality conditions on braided and diagonal categories...
commit | commitdiff | tree
2011-03-25 Adam Megaczbase CartesianCat on MonoidalCat, not PreMonoidalCat
 commit | commitdiff | tree
2011-03-25 Adam Megaczupdate imports in EquivalentCategories
 commit | commitdiff | tree
2011-03-25 Adam Megaczremove CategoryOfCategories, which isnt ready yet
 commit | commitdiff | tree
2011-03-22 Adam Megaczmake the codomain of the FreydCategory functor a parameter...
commit | commitdiff | tree
2011-03-21 Adam Megaczadd formalization of Arrows and Freyd Categories
 commit | commitdiff | tree
2011-03-21 Adam Megaczrename General/Preamble to avoid conflict with ghc...
commit | commitdiff | tree
2011-03-11 Adam Megaczinitial checkin of coq-categories library
 commit | commitdiff | tree
formalization of basic category theory in Coq