Commits

History for

Commits on May 8, 2015

patch by Jason for case sensitive file systems
spitters
committed

Commits on Sep 21, 2014

Sources are at the root
clarus
committed

Commits on Jul 7, 2010

Move sources into src/.
Eelis
committed

Commits on Apr 9, 2010

categories/cat: Simplify functor equality.
Eelis
committed

Commits on Mar 27, 2010

Add Category fields to Functor; add Functor fields to Adjunction. Also clean up theory/adjunctions.
Eelis
committed

Commits on Mar 5, 2010

Clean up parts once made ugly for universe consistency reasons that I cannot reproduce. Better describe part where universe consistency problem really exists. Remove pointless categorical object de…
Eelis
committed

Commits on Feb 22, 2010

Make compile with Coq trunk 12801, and use its unification improvements to clean up several proofs.
Eelis
committed

Commits on Feb 21, 2010

Use nice notations. Clean up proofs and definitions. Add alternative definition of adjunctions by universal morphisms and show freedom coincides.
Eelis
committed

Commits on Feb 17, 2010

Use notation for arrow composition. Add class for natural transformations.
Eelis
committed

Commits on Feb 16, 2010

Lots and lots of cleanup. Add type classes for arrows and functors' arrow maps. Make many instances nameless.
Eelis
committed

Commits on Feb 12, 2010

Recognize algebras (without entailments) as distinguished structure. Lots of other changes.
Eelis
committed

Commits on Jan 2, 2010

Make compatible with latest Coq trunk (needed because of new type class fixes). In interfaces/universal_algebra: remove unused things, clean up, better names, more documentation.
Eelis
committed

Commits on Dec 27, 2009

Add many category-theory/universal-algebra notions (e.g. initiality, free objects, products) and theory (e.g. generation of initial objects and products in variety categories) and lots of instances…
Eelis
committed

Loading