Commits

Breadcrumbs

History for

onmaster

User selector

All users

Datepicker

All time

Commit History

Commits on Feb 23, 2018

• Change Implicit Arguments to Arguments

  jashug

  committed
  5b7cb6d

Commits on Jun 15, 2016

• Fix for new typeclasses eauto.

  mattam82

  committed
  4d921ee

Commits on Apr 20, 2016

• merging with origin/trunk

  

  Matej Kosik

  committed
  3f5404a

Commits on Apr 19, 2016

• Fix compilation

  

  ppedrot

  authored and

  Matej Kosik

  committed
  78856a5

Commits on Mar 1, 2016

• merged Coq team's fixes to mathclasses, from branch v8.5 at

  Show description for 37ba73a
  aa755

  committed
  37ba73a

Commits on May 8, 2015

• patch by Jason for case sensitive file systems

  spitters

  committed
  9330ab1

Commits on Sep 21, 2014

• Sources are at the root

  clarus

  committed
  7770150

Commits on Jul 7, 2010

• Move sources into src/.

  Eelis

  committed
  2eb03d8

Commits on Jun 16, 2010

• Add category of functors with natural transformations between them.

  

  tomprince

  authored and

  Eelis

  committed
  7460b2f

Commits on May 5, 2010

• Add monoid quotation and equation solver. Universal algebra: use ne_list for optypes, packed terms w/ conversion and ind. principles; lots of cleanup.

  Eelis

  committed
  6006ee4

Commits on Apr 23, 2010

• Add variant of CAT with functor equality defined in terms of Leibniz (for objects) and JMrelation (for arrows).

  Eelis

  committed
  c300268

Commits on Apr 9, 2010

• categories/cat: Simplify functor equality.

  Eelis

  committed
  dafbfdf

Commits on Mar 27, 2010

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

  Eelis

  committed
  9c7f221

Commits on Mar 21, 2010

• Rename Variety → InVariety.

  Eelis

  committed
  c3157e0

Commits on Mar 19, 2010

• Different treatment of injections/surjections/bijections. Sync with Coq trunk. Other minor changes.

  Eelis

  committed
  07c150c

Commits on Mar 7, 2010

• Make compile with Coq trunk 12850.

  

  Eelis

  committed
  5a65f46

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…

  Show description for 90feab6
  Eelis

  committed
  90feab6

Commits on Feb 26, 2010

• Proper type-classified treatment of products.

  Eelis

  committed
  8f0ece4

Commits on Feb 22, 2010

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

  Eelis

  committed
  6da1cb3

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
  2c31457

Commits on Feb 17, 2010

• Use notation for arrow composition. Add class for natural transformations.

  Eelis

  committed
  bff411b

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
  f6fbfd3

Commits on Feb 12, 2010

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

  Eelis

  committed
  58e36f0

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
  8619476

Commits on Dec 28, 2009

• Make code compile with Coq trunk r12609 and use its newly introduced [Global Existing Instance].

  Eelis

  committed
  c95ab72

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…

  Show description for b3ea259
  Eelis

  committed
  b3ea259

Loading