major revision: MonoidalCat is now a subclass of PreMonoidalCat
[coq-categories.git] / src /
2011-04-03 Adam Megaczmajor revision: MonoidalCat is now a subclass of PreMon...
2011-04-02 Adam Megaczsplit MonoidalCategories into Binoidal and PreMonoidal
2011-04-02 Adam Megaczadd isos_forward_equal_then_backward_equal, iso_inv_inv
2011-03-29 Adam Megaczfinish the proof of ffc_functor_weakly_monic
2011-03-29 Adam Megaczfurther work on CenterMonoidal
2011-03-29 Adam Megaczcomment out unused portion of RepresentableStructure_ch7_2
2011-03-29 Adam Megaczrename RepresentableFunctor to HomFunctor
2011-03-28 Adam Megaczmake mf_compose_coherence transparent
2011-03-27 Adam MegaczIsomorphicCategories: make the components fields, not...
2011-03-27 Adam Megaczadd SurjectiveEnrichment to SMME
2011-03-27 Adam Megaczpartial implementation of MonoidalFunctorsCompose
2011-03-26 Adam Megaczfix typo
2011-03-26 Adam Megaczadd Retraction, SMME, make Enrichment a parameter
2011-03-25 Adam Megaczadd func_diagonal, fix naturality for DiagonalCat
2011-03-25 Adam Megaczfix Freyd Categories
2011-03-25 Adam Megaczfix naturality conditions on braided and diagonal categ...
2011-03-25 Adam Megaczbase CartesianCat on MonoidalCat, not PreMonoidalCat
2011-03-25 Adam Megaczupdate imports in EquivalentCategories
2011-03-25 Adam Megaczremove CategoryOfCategories, which isnt ready yet
2011-03-22 Adam Megaczmake the codomain of the FreydCategory functor a parame...
2011-03-21 Adam Megaczadd formalization of Arrows and Freyd Categories
2011-03-21 Adam Megaczrename General/Preamble to avoid conflict with ghc...
2011-03-11 Adam Megaczinitial checkin of coq-categories library