projects / coq-categories.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2064145) | patch
FullSubcategoryInclusionFunctor for a monoidal subcategory is monoidal
authorAdam Megacz <megacz@cs.berkeley.edu>
Mon, 11 Apr 2011 03:15:40 +0000 (03:15 +0000)
committerAdam Megacz <megacz@cs.berkeley.edu>
Mon, 11 Apr 2011 03:15:40 +0000 (03:15 +0000)
commitfd14c25703d15bd78088c67ff3d417d435b6b136
treefd73c7be30c427484445c70dff1e7bdaf5a16c38tree | snapshot
parent20641452e40570b4bfc9429ca57b0cffca6eccfbcommit | diff
FullSubcategoryInclusionFunctor for a monoidal subcategory is monoidal
src/PreMonoidalCategories.v diff | blob | history
formalization of basic category theory in Coq