coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Inductive types and isomorphisms....

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Inductive types and isomorphisms....
Date: Wed, 9 May 2018 08:43:52 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga09.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:SYH3VBJ8dGGkHoVxtdmcpTZWNBhigK39O0sv0rFitYgeL/7xwZ3uMQTl6Ol3ixeRBMOHs6kC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwtFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhicZOTAk7GHZhM9+jKxZrxKguxNwzIHabZqJNPVleq7RYc8WSXZDU8tXSidPApm8b4wKD+cZM+pWso79qEUBrRuiHwmsA/vvxidVjXHx3K01z+QhHhvY0wwkEd4FrXPZrND0NKgOUeC61rfHzTHZY/NN3jfy9ofIcgw7ofGLRbJ9asvRyU8zFwzbilWcs5DqPzSQ1ukUtWWQ8uRuVeWqi2E9qgFxpCCixsYqionVmI0VzkrI+jhnz4szONa2S1Z7bMa5HJZeuCyWLZZ6T80tTm1ypSo3xLwLtYSlcCUF0Jgr2h/SZvKdf4WG7B/vTvidLDl8iX5/Zb6yhAu+/VC9xuD9UsS4ykhGoypKn9XWqHwBzQLf58eDR/Z740yvwyyA1xrJ5eFBOU00lbTUK5omwrMok5oTvl7MEjPylUnsja+WcFkk9fas6+j9frrmoZqcO5d1igH4LKsuhtSyDfk2PwUBRWSX5Oqx2bL58UHkTrhHj+c6nrfWvZzCIMQUvK+5Awtb0oY57Ba/Ci+r0NEZnXYbLFJKYgyIj4zzN1HVJ/D3E/i/g0i2kDds3/DLJbzhApPRLnfdlLftZ6py60lZyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiipzklgEOKKtwJE/aXaiH/0gLV/TKS7nhc5EGmMXtCI/SvbrgRuMS2gASWy1Wvd23TY2B568Cp+HDqWsi7yI0SPxVslTZ2tGA12IV2zveoqYQfAUQCOUPsJl1DcDUO7yGMcayRiyuVqimPJcJe3O93hA7MOx5J1O/+TW0CoK23lxBsWZ3XuKSjgtzGIOWzIymqt4pB4kkwvR4e1Dm/VdUOdrybZRSA5jbMzdyfB3D5b5XQeTJo7UGmbjec2vBHQKdvx0w9IKZB8iSdCth0iSmSusH7IR0beMAc5s/w==

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

[Coq-Club] Inductive types and isomorphisms...., Fred Smith, 05/06/2018
- Re: [Coq-Club] Inductive types and isomorphisms...., Gaëtan Gilbert, 05/06/2018
  - Re: [Coq-Club] Inductive types and isomorphisms...., José Manuel Rodriguez Caballero, 05/06/2018
- Re: [Coq-Club] Inductive types and isomorphisms...., Morrisett, 05/06/2018
  - Re: [Coq-Club] Inductive types and isomorphisms...., Fred Smith, 05/07/2018
- Re: [Coq-Club] Inductive types and isomorphisms...., James Lottes, 05/07/2018
  - Re: [Coq-Club] Inductive types and isomorphisms...., Matthieu Sozeau, 05/08/2018
    - RE: [Coq-Club] Inductive types and isomorphisms...., Soegtrop, Michael, 05/08/2018
      - Re: [Coq-Club] Inductive types and isomorphisms...., Bas Spitters, 05/08/2018
        
        RE: [Coq-Club] Inductive types and isomorphisms...., Soegtrop, Michael, 05/09/2018
        
        Re: [Coq-Club] Inductive types and isomorphisms...., Bas Spitters, 05/09/2018
        
        Re: [Coq-Club] Inductive types and isomorphisms...., Théo Zimmermann, 05/09/2018