add inverse form of ni_commutes
[coq-categories.git] / src / Subcategories_ch7_1.v
2011-04-11 Adam Megaczadd FullSubcategoryInclusionFunctor
2011-04-10 Adam Megaczadd natural-iso form of RestrictToImage_splits
2011-04-09 Adam Megaczadd RestrictDomain
2011-04-06 Adam Megaczuncomment FullImage development
2011-04-06 Adam Megaczadd Notations.v
2011-04-05 Adam Megaczformatting fixes
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-03-29 Adam Megaczfinish the proof of ffc_functor_weakly_monic
2011-03-11 Adam Megaczinitial checkin of coq-categories library