The Coq mailing list

[Bas Spitters <spitters AT cs.ru.nl>]

We have some order theory, basic universal algebra and basic category theory here:

http://math-classes.org/

This is explained in our papers:
Type classes for efficient exact real arithmetic in Coq (with Robbert Krebbers)
http://www.lmcs-online.org/ojs/viewarticle.php?id=987&layout=abstract

Type Classes for Mathematics in Type Theory (with Eelis van der Weegen).
http://dx.doi.org/10.1017/S0960129511000119

On Mon, Nov 18, 2013 at 8:28 AM, <Patrick.Barlatier AT univ-savoie.fr> wrote:

Hi all,
Is there anyone aware of an existing library written in Coq with type classes about lattices?
Thanks in advance for your help.
Patrick