2011-04-11 |
Adam Megacz | add FullSubcategoryInclusionFunctor |
commit | commitdiff | tree | snapshot |
2011-04-11 |
Adam Megacz | make EBinoidalCat action-on-objects a parameter instead... |
commit | commitdiff | tree | snapshot |
2011-04-10 |
Adam Megacz | add natural-iso form of RestrictToImage_splits |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | FreydCategories: add strictness requirement for unit... |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | Isomorphisms: add alternative forms, useful for rewriting |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | add functor_comp_assoc |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | add a notation for composition of isomorphisms |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | finish implementation of PreMonoidalFullsubcategory |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | add RestrictDomain |
commit | commitdiff | tree | snapshot |
2011-04-09 |
Adam Megacz | add MonoidalNaturalIsomorphism, MonoidalEquivalence... |
commit | commitdiff | tree | snapshot |
2011-04-06 |
Adam Megacz | uncomment FullImage development |
commit | commitdiff | tree | snapshot |
2011-04-06 |
Adam Megacz | add Notations.v |
commit | commitdiff | tree | snapshot |
2011-04-06 |
Adam Megacz | remove reliance on General.v |
commit | commitdiff | tree | snapshot |
2011-04-06 |
Adam Megacz | make the Functor of {Pre}MonoidalFunctor a parameter... |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | PreMonoidalCategories: remove the very last [[admit]] |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | add special case of ni_respects where one side is exact... |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | rename Retraction to RetractionOfCategories |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | formatting fixes |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | remove Arrows.v |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | fix miscompilation errors introduced by recent changes |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | flip around the pentagon to the opposite of Mac Lane... |
commit | commitdiff | tree | snapshot |
2011-04-05 |
Adam Megacz | add proof of MacLane_ex_VII_1_1 |
commit | commitdiff | tree | snapshot |
2011-04-04 |
Adam Megacz | major revision: separate Subcategory into {Wide,Full... |
commit | commitdiff | tree | snapshot |
2011-04-03 |
Adam Megacz | major revision: MonoidalCat is now a subclass of PreMon... |
commit | commitdiff | tree | snapshot |
2011-04-03 |
Adam Megacz | Makefile: insist on native-compiled Coq |
commit | commitdiff | tree | snapshot |
2011-04-03 |
Adam Megacz | add README |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | split MonoidalCategories into Binoidal and PreMonoidal |
commit | commitdiff | tree | snapshot |
2011-04-02 |
Adam Megacz | add isos_forward_equal_then_backward_equal, iso_inv_inv |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | finish the proof of ffc_functor_weakly_monic |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | further work on CenterMonoidal |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | comment out unused portion of RepresentableStructure_ch7_2 |
commit | commitdiff | tree | snapshot |
2011-03-29 |
Adam Megacz | rename RepresentableFunctor to HomFunctor |
commit | commitdiff | tree | snapshot |
2011-03-28 |
Adam Megacz | make mf_compose_coherence transparent |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | IsomorphicCategories: make the components fields, not... |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | add SurjectiveEnrichment to SMME |
commit | commitdiff | tree | snapshot |
2011-03-27 |
Adam Megacz | partial implementation of MonoidalFunctorsCompose |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | fix typo |
commit | commitdiff | tree | snapshot |
2011-03-26 |
Adam Megacz | add Retraction, SMME, make Enrichment a parameter |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | add func_diagonal, fix naturality for DiagonalCat |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | fix Freyd Categories |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | fix naturality conditions on braided and diagonal categ... |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | base CartesianCat on MonoidalCat, not PreMonoidalCat |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | update imports in EquivalentCategories |
commit | commitdiff | tree | snapshot |
2011-03-25 |
Adam Megacz | remove CategoryOfCategories, which isnt ready yet |
commit | commitdiff | tree | snapshot |
2011-03-22 |
Adam Megacz | make the codomain of the FreydCategory functor a parame... |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | add formalization of Arrows and Freyd Categories |
commit | commitdiff | tree | snapshot |
2011-03-21 |
Adam Megacz | rename General/Preamble to avoid conflict with ghc... |
commit | commitdiff | tree | snapshot |
2011-03-11 |
Adam Megacz | initial checkin of coq-categories library |
commit | commitdiff | tree | snapshot |
|