coq-categories.git
9 years agoadd inverse form of ni_commutes master
Adam Megacz [Sun, 24 Apr 2011 07:00:24 +0000 (00:00 -0700)]
add inverse form of ni_commutes

9 years agoadd MonoidalFullSubcategory_Monoidal
Adam Megacz [Mon, 11 Apr 2011 04:26:55 +0000 (04:26 +0000)]
add MonoidalFullSubcategory_Monoidal

9 years agoFullSubcategoryInclusionFunctor for a monoidal subcategory is monoidal
Adam Megacz [Mon, 11 Apr 2011 03:15:40 +0000 (03:15 +0000)]
FullSubcategoryInclusionFunctor for a monoidal subcategory is monoidal

9 years agoadd FullSubcategoryInclusionFunctor
Adam Megacz [Mon, 11 Apr 2011 03:15:21 +0000 (03:15 +0000)]
add FullSubcategoryInclusionFunctor

9 years agomake EBinoidalCat action-on-objects a parameter instead of field
Adam Megacz [Mon, 11 Apr 2011 02:36:25 +0000 (02:36 +0000)]
make EBinoidalCat action-on-objects a parameter instead of field

9 years agoadd natural-iso form of RestrictToImage_splits
Adam Megacz [Sun, 10 Apr 2011 03:55:48 +0000 (03:55 +0000)]
add natural-iso form of RestrictToImage_splits

9 years agoFreydCategories: add strictness requirement for unit object
Adam Megacz [Sat, 9 Apr 2011 09:00:03 +0000 (09:00 +0000)]
FreydCategories: add strictness requirement for unit object

9 years agoIsomorphisms: add alternative forms, useful for rewriting
Adam Megacz [Sat, 9 Apr 2011 08:52:38 +0000 (08:52 +0000)]
Isomorphisms: add alternative forms, useful for rewriting

9 years agoadd functor_comp_assoc
Adam Megacz [Sat, 9 Apr 2011 03:55:27 +0000 (03:55 +0000)]
add functor_comp_assoc

9 years agoadd a notation for composition of isomorphisms
Adam Megacz [Sat, 9 Apr 2011 03:18:59 +0000 (03:18 +0000)]
add a notation for composition of isomorphisms

9 years agofinish implementation of PreMonoidalFullsubcategory
Adam Megacz [Sat, 9 Apr 2011 02:51:09 +0000 (02:51 +0000)]
finish implementation of PreMonoidalFullsubcategory

9 years agoadd RestrictDomain
Adam Megacz [Sat, 9 Apr 2011 02:44:57 +0000 (02:44 +0000)]
add RestrictDomain

9 years agoadd MonoidalNaturalIsomorphism, MonoidalEquivalence, MonoidalNaturalEquivalence
Adam Megacz [Sat, 9 Apr 2011 02:44:31 +0000 (02:44 +0000)]
add MonoidalNaturalIsomorphism, MonoidalEquivalence, MonoidalNaturalEquivalence

9 years agouncomment FullImage development
Adam Megacz [Wed, 6 Apr 2011 09:59:27 +0000 (09:59 +0000)]
uncomment FullImage development

9 years agoadd Notations.v
Adam Megacz [Wed, 6 Apr 2011 07:22:14 +0000 (07:22 +0000)]
add Notations.v

9 years agoremove reliance on General.v
Adam Megacz [Wed, 6 Apr 2011 04:48:06 +0000 (04:48 +0000)]
remove reliance on General.v

9 years agomake the Functor of {Pre}MonoidalFunctor a parameter rather than a field
Adam Megacz [Wed, 6 Apr 2011 04:26:37 +0000 (04:26 +0000)]
make the Functor of {Pre}MonoidalFunctor a parameter rather than a field

9 years agoPreMonoidalCategories: remove the very last [[admit]]
Adam Megacz [Tue, 5 Apr 2011 06:33:20 +0000 (06:33 +0000)]
PreMonoidalCategories: remove the very last [[admit]]

9 years agoadd special case of ni_respects where one side is exactly equal
Adam Megacz [Tue, 5 Apr 2011 06:32:52 +0000 (06:32 +0000)]
add special case of ni_respects where one side is exactly equal

9 years agorename Retraction to RetractionOfCategories
Adam Megacz [Tue, 5 Apr 2011 06:32:20 +0000 (06:32 +0000)]
rename Retraction to RetractionOfCategories

9 years agoformatting fixes
Adam Megacz [Tue, 5 Apr 2011 06:32:04 +0000 (06:32 +0000)]
formatting fixes

9 years agoremove Arrows.v
Adam Megacz [Tue, 5 Apr 2011 06:31:50 +0000 (06:31 +0000)]
remove Arrows.v

9 years agofix miscompilation errors introduced by recent changes
Adam Megacz [Tue, 5 Apr 2011 02:55:10 +0000 (02:55 +0000)]
fix miscompilation errors introduced by recent changes

9 years agoflip around the pentagon to the opposite of Mac Lane orientation
Adam Megacz [Tue, 5 Apr 2011 02:05:21 +0000 (02:05 +0000)]
flip around the pentagon to the opposite of Mac Lane orientation

9 years agoadd proof of MacLane_ex_VII_1_1
Adam Megacz [Mon, 4 Apr 2011 23:51:53 +0000 (23:51 +0000)]
add proof of MacLane_ex_VII_1_1

9 years agomajor revision: separate Subcategory into {Wide,Full}Subcategory
Adam Megacz [Mon, 4 Apr 2011 02:06:03 +0000 (02:06 +0000)]
major revision: separate Subcategory into {Wide,Full}Subcategory

9 years agomajor revision: MonoidalCat is now a subclass of PreMonoidalCat
Adam Megacz [Sun, 3 Apr 2011 04:57:51 +0000 (04:57 +0000)]
major revision: MonoidalCat is now a subclass of PreMonoidalCat

9 years agoMakefile: insist on native-compiled Coq
Adam Megacz [Sun, 3 Apr 2011 04:09:12 +0000 (04:09 +0000)]
Makefile: insist on native-compiled Coq

9 years agoadd README
Adam Megacz [Sun, 3 Apr 2011 04:08:55 +0000 (04:08 +0000)]
add README

9 years agosplit MonoidalCategories into Binoidal and PreMonoidal
Adam Megacz [Sat, 2 Apr 2011 22:48:40 +0000 (15:48 -0700)]
split MonoidalCategories into Binoidal and PreMonoidal

9 years agoadd isos_forward_equal_then_backward_equal, iso_inv_inv
Adam Megacz [Sat, 2 Apr 2011 20:17:18 +0000 (13:17 -0700)]
add isos_forward_equal_then_backward_equal, iso_inv_inv

9 years agofinish the proof of ffc_functor_weakly_monic
Adam Megacz [Tue, 29 Mar 2011 13:35:38 +0000 (06:35 -0700)]
finish the proof of ffc_functor_weakly_monic

9 years agofurther work on CenterMonoidal
Adam Megacz [Tue, 29 Mar 2011 13:35:23 +0000 (06:35 -0700)]
further work on CenterMonoidal

9 years agocomment out unused portion of RepresentableStructure_ch7_2
Adam Megacz [Tue, 29 Mar 2011 13:34:59 +0000 (06:34 -0700)]
comment out unused portion of RepresentableStructure_ch7_2

9 years agorename RepresentableFunctor to HomFunctor
Adam Megacz [Tue, 29 Mar 2011 11:37:57 +0000 (04:37 -0700)]
rename RepresentableFunctor to HomFunctor

9 years agomake mf_compose_coherence transparent
Adam Megacz [Mon, 28 Mar 2011 00:23:40 +0000 (17:23 -0700)]
make mf_compose_coherence transparent

9 years agoIsomorphicCategories: make the components fields, not methods
Adam Megacz [Sun, 27 Mar 2011 19:22:28 +0000 (12:22 -0700)]
IsomorphicCategories: make the components fields, not methods

9 years agoadd SurjectiveEnrichment to SMME
Adam Megacz [Sun, 27 Mar 2011 19:22:12 +0000 (12:22 -0700)]
add SurjectiveEnrichment to SMME

9 years agopartial implementation of MonoidalFunctorsCompose
Adam Megacz [Sun, 27 Mar 2011 02:13:15 +0000 (19:13 -0700)]
partial implementation of MonoidalFunctorsCompose

9 years agofix typo
Adam Megacz [Sat, 26 Mar 2011 08:39:02 +0000 (01:39 -0700)]
fix typo

9 years agoadd Retraction, SMME, make Enrichment a parameter
Adam Megacz [Sat, 26 Mar 2011 07:06:26 +0000 (00:06 -0700)]
add Retraction, SMME, make Enrichment a parameter

9 years agoadd func_diagonal, fix naturality for DiagonalCat
Adam Megacz [Fri, 25 Mar 2011 23:41:07 +0000 (16:41 -0700)]
add func_diagonal, fix naturality for DiagonalCat

9 years agofix Freyd Categories
Adam Megacz [Fri, 25 Mar 2011 23:16:27 +0000 (16:16 -0700)]
fix Freyd Categories

9 years agofix naturality conditions on braided and diagonal categories, add CenterMonoidal
Adam Megacz [Fri, 25 Mar 2011 23:16:19 +0000 (16:16 -0700)]
fix naturality conditions on braided and diagonal categories, add CenterMonoidal

9 years agobase CartesianCat on MonoidalCat, not PreMonoidalCat
Adam Megacz [Fri, 25 Mar 2011 18:18:51 +0000 (11:18 -0700)]
base CartesianCat on MonoidalCat, not PreMonoidalCat

9 years agoupdate imports in EquivalentCategories
Adam Megacz [Fri, 25 Mar 2011 16:59:25 +0000 (09:59 -0700)]
update imports in EquivalentCategories

9 years agoremove CategoryOfCategories, which isnt ready yet
Adam Megacz [Fri, 25 Mar 2011 16:58:55 +0000 (09:58 -0700)]
remove CategoryOfCategories, which isnt ready yet

9 years agomake the codomain of the FreydCategory functor a parameter rather than a field
Adam Megacz [Tue, 22 Mar 2011 00:45:46 +0000 (17:45 -0700)]
make the codomain of the FreydCategory functor a parameter rather than a field

9 years agoadd formalization of Arrows and Freyd Categories
Adam Megacz [Mon, 21 Mar 2011 01:53:23 +0000 (18:53 -0700)]
add formalization of Arrows and Freyd Categories

9 years agorename General/Preamble to avoid conflict with ghc-hetmet
Adam Megacz [Mon, 21 Mar 2011 01:53:02 +0000 (18:53 -0700)]
rename General/Preamble to avoid conflict with ghc-hetmet

9 years agoinitial checkin of coq-categories library
Adam Megacz [Fri, 11 Mar 2011 07:59:30 +0000 (23:59 -0800)]
initial checkin of coq-categories library