add inverse form of ni_commutes
[coq-categories.git] / src / MonoidalCategories_ch7_8.v
2011-04-11 Adam Megaczadd MonoidalFullSubcategory_Monoidal
2011-04-09 Adam Megaczfinish implementation of PreMonoidalFullsubcategory
2011-04-09 Adam Megaczadd MonoidalNaturalIsomorphism, MonoidalEquivalence...
2011-04-06 Adam Megaczadd Notations.v
2011-04-06 Adam Megaczmake the Functor of {Pre}MonoidalFunctor a parameter...
2011-04-04 Adam Megaczmajor revision: separate Subcategory into {Wide,Full...
2011-04-03 Adam Megaczmajor revision: MonoidalCat is now a subclass of PreMon...
2011-04-02 Adam Megaczsplit MonoidalCategories into Binoidal and PreMonoidal
2011-03-29 Adam Megaczfurther work on CenterMonoidal
2011-03-28 Adam Megaczmake mf_compose_coherence transparent
2011-03-27 Adam Megaczpartial implementation of MonoidalFunctorsCompose
2011-03-25 Adam Megaczadd func_diagonal, fix naturality for DiagonalCat
2011-03-25 Adam Megaczfix naturality conditions on braided and diagonal categ...
2011-03-25 Adam Megaczbase CartesianCat on MonoidalCat, not PreMonoidalCat
2011-03-11 Adam Megaczinitial checkin of coq-categories library