The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi,

Connecting lemmas "after the fact" and being able to transfer theorems when we have less than isomorphisms were precisely two of the goals of my transfer library: https://github.com/Zimmi48/transfer

It would still need more work but can still be used (played with) as of today.

CoqEAL and the parametricity plugin were already cited in this thread and the general principles behind all these are basically the same. However, AFAIK CoqEAL is not really usable as of today (it was being rewritten using the parametricity plugin). As for the parametricity plugin, is there a small tutorial on how to use it to do theorem transfer?

Thanks,

Théo

Le mer. 9 mai 2018 à 11:18, Bas Spitters <b.a.w.spitters AT gmail.com> a écrit :

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