descriptionformalization of basic category theory in Coq
last changeSun, 24 Apr 2011 07:00:24 +0000 (00:00 -0700)
2011-04-24 Adam Megaczadd inverse form of ni_commutes master
2011-04-11 Adam Megaczadd MonoidalFullSubcategory_Monoidal
2011-04-11 Adam MegaczFullSubcategoryInclusionFunctor for a monoidal subcateg...
2011-04-11 Adam Megaczadd FullSubcategoryInclusionFunctor
2011-04-11 Adam Megaczmake EBinoidalCat action-on-objects a parameter instead...
2011-04-10 Adam Megaczadd natural-iso form of RestrictToImage_splits
2011-04-09 Adam MegaczFreydCategories: add strictness requirement for unit...
2011-04-09 Adam MegaczIsomorphisms: add alternative forms, useful for rewriting
2011-04-09 Adam Megaczadd functor_comp_assoc
2011-04-09 Adam Megaczadd a notation for composition of isomorphisms
2011-04-09 Adam Megaczfinish implementation of PreMonoidalFullsubcategory
2011-04-09 Adam Megaczadd RestrictDomain
2011-04-09 Adam Megaczadd MonoidalNaturalIsomorphism, MonoidalEquivalence...
2011-04-06 Adam Megaczuncomment FullImage development
2011-04-06 Adam Megaczadd Notations.v
2011-04-06 Adam Megaczremove reliance on General.v
13 years ago master