git.megacz.com Git - coq-categories.git/search

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

formalization of basic category theory in Coq

RSS Atom