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