Math Classes

math-classes is a library of abstract interfaces for mathematical structures.

• Algebraic hierarchy (groups, rings, fields, ...)
• Relations, orders, ...
• Categories, functors, universal algebra, ...
• Numbers: NN, ZZ, QQ, ...
• Operations, ...

It's heavily based on Coq's Type Classes in order to achieve:

• elegant and mathematically sound abstract interfaces for algebraic and numeric structures up to and including rationals (with practical use of universal algebra and category theory);
• a very flexible purely predicate-based representation of algebraic structures that makes sharing, multiple inheritance, and derived inheritance, all trivial;
• clean expression terms that neither refer to proofs nor require deeply nested record projections;
• fluent rewriting;
• easy and flexible replacement and specialization of data representations and operations with more efficient versions;
• ordinary mathematical notation and overloaded names not reliant on Coq's notation scopes.

More information can be found here:

Presentation Paper

You can find the latest code on github