git.megacz.com Git - coq-categories.git/atom - src historyformalization of basic category theory in Coqhttp://git.megacz.com/?p=coq-categories.git/git-favicon.png/git-logo.png2011-04-24T07:00:24Zgitwebadd inverse form of ni_commutes2011-04-24T07:00:24ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-24T07:00:24Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=422dab8d300548c294b95c0f4bbf27aecadbd745
FullSubcategoryInclusionFunctor for a monoidal subcategory is monoidal2011-04-11T03:15:40ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-11T03:15:40Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=fd14c25703d15bd78088c67ff3d417d435b6b136
FullSubcategoryInclusionFunctor for a monoidal subcategory is monoidal
make EBinoidalCat action-on-objects a parameter instead of field2011-04-11T02:36:25ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-11T02:36:25Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=f494aec0e2a8f5ccb7a5f560dd4f8a0b302feb40
make EBinoidalCat action-on-objects a parameter instead of field
add natural-iso form of RestrictToImage_splits2011-04-10T03:55:48ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-10T03:55:48Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=1104780d775bf36ff9f44ab287c22604ab47f0b5
FreydCategories: add strictness requirement for unit object2011-04-09T09:00:03ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-09T09:00:03Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=658181bed516646957267b055341d9d4b197ed0d
FreydCategories: add strictness requirement for unit object
Isomorphisms: add alternative forms, useful for rewriting2011-04-09T08:52:38ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-09T08:52:38Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=57dfee583c84915cb6b3aadfa1dba692681499b3
Isomorphisms: add alternative forms, useful for rewriting
add a notation for composition of isomorphisms2011-04-09T03:18:59ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-09T03:18:59Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=469c709f122da80a207769aab3cd038fd1c3d509
make the Functor of {Pre}MonoidalFunctor a parameter rather than a field2011-04-06T04:26:37ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-06T04:26:37Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=9acb9b7b4ed12543e54c39c82d7b0f34d04d0207
make the Functor of {Pre}MonoidalFunctor a parameter rather than a field
PreMonoidalCategories: remove the very last [[admit]]2011-04-05T06:33:20ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-05T06:33:20Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=5f3bdb7947de02d8d60f1af77c999a3c80f7dbba
PreMonoidalCategories: remove the very last [[admit]]
add special case of ni_respects where one side is exactly equal2011-04-05T06:32:52ZAdam Megaczmegacz@cs.berkeley.eduAdam Megaczmegacz@cs.berkeley.edu2011-04-05T06:32:52Zhttp://git.megacz.com/?p=coq-categories.git;a=commitdiff;h=e6eee3c9787855479899acb82cb65f9cdd0259c6
add special case of ni_respects where one side is exactly equal