The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Yes, that seems fair.

There's a partial port of math-classes to hott, but it doesn't include
universal algebra yet.

https://github.com/HoTT/HoTT/tree/master/theories/Classes

Best,

Bas

On Wed, May 9, 2018 at 10:43 AM, Soegtrop, Michael
<michael.soegtrop AT intel.com>
 wrote:
> Dear Bas,
>
> as far as I understand the technique you describe would work for my case if 
> the number and expression types I use would be defined based on the 
> universal algebra / algebraic structures you define in your development. 
> But it wouldn't work for e.g. connecting the algebra of number types 
> defined in the Coq standard library to the algebra of expression types 
> defined in my development based on arbitrary foundations "after the facts".
>
> Also as far as I understood the univalence based work Matthieu referenced 
> does allow to connect structures "after the facts".
>
> Is this understanding approximately correct?
>
> Still it would be an absolutely reasonable option to base both numbers and 
> expression types on your universal algebra developments.
>
> Best regards,
>
> Michael
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928