Permalink
Switch branches/tags
Nothing to show
Commits on Mar 30, 2012
Commits on Feb 3, 2012
Commits on Feb 2, 2012
  1. Merge branch 'future' of git://github.com/tomprince/math-classes

    robbertkrebbers committed Feb 2, 2012
    Conflicts:
    	src/interfaces/abstract_algebra.v
    	src/interfaces/canonical_names.v
    	src/theory/forget_algebra.v
  2. Merge branch 'master' of git://github.com/tomprince/math-classes

    robbertkrebbers committed Feb 2, 2012
    Conflicts:
    	src/categories/functors.v
  3. Add some automation.

    robbertkrebbers committed Feb 2, 2012
  4. Put all notations in a scope: mc_scope. This is convenient for develo…

    robbertkrebbers committed Feb 2, 2012
    …pments that do use scopes and want to incorporate math-classes.
  5. Improve interfaces for monads. Prove that list is a monad (which does…

    robbertkrebbers committed Feb 2, 2012
    … not give universe inconsistencies anymore).
  6. Misc small patches.

    robbertkrebbers committed Feb 2, 2012
  7. Update README

    robbertkrebbers committed Feb 2, 2012
Commits on Jan 10, 2012
Commits on Nov 24, 2011
  1. Add varieties/abgroup.

    tomprince committed Nov 24, 2011
  2. Some cleanups.

    tomprince committed Nov 24, 2011
  3. Import coercions by default.

    tomprince committed Nov 24, 2011
  4. Add categories.orders.

    tomprince committed Sep 6, 2011
  5. Hint Resolve order_preserving.

    tomprince committed Sep 6, 2011
    But actually deduce the appropriate function so that it works.
  6. Add constant functors/natural transformation.

    tomprince committed Jun 16, 2010
    Reformatting by Robbert Krebbers.
  7. Generalize ext_equiv_trans and ext_equiv_sym.

    tomprince committed Nov 24, 2011
    We don't need the source and target to be Setoids, so just use
    the weaker requirement.
  8. bit of cleanup

    wires committed Nov 24, 2011
  9. update README

    robbertkrebbers committed Nov 24, 2011
Commits on Nov 23, 2011
  1. Give a name to the Arrows instance in categories.setoid.

    tomprince committed Apr 27, 2011
    This is needed because of unification problems.
    
    Signed-off-by: Tom Prince <tom.prince@ualberta.net>