coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Coq universes

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Question about Coq universes
Date: Wed, 22 Apr 2020 17:12:56 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay9-d.mail.gandi.net
Ironport-phdr: 9a23:upy0vx+wMrk8hP9uRHKM819IXTAuvvDOBiVQ1KB30OscTK2v8tzYMVDF4r011RmVBNidt60P1LqempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgVFiCCybL5wIxm7rwbcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh7W/ZlMJwgqJYrhyvqRNwzIzbb52aOvdlYqPQfskXSXZdUstfVSFMBJ63YYsVD+oGOOZVt4jzqEESqhuiHwasAvvgxD5Jhn/yxqI1zf4hER3b1wEnENIBqmrbrMnvO6cUS+y1w6jIzTHYYPxIwzf99JPFcgsiofCMRrJwcsvRyUwqFwzblFWcs4rlMC2J1ukUtWWQ8uRuVeWqi2E9qgFxpCCixtoqionImIIZ00vE9SBiz4ovK924Ukh2asOnHptIryyWKZZ6T8E4T2xqpCo20KAKtJ21cSQQ1ZgqwxrSZ+SZf4SV7B/vTvudLDdmiH5/Zb6yhgu+/VK9xuD8UMS/zUxEoTBfktbWs3AAzxzT5daDSvt65kqhwyiA1wTJ5eBEJU04jLfUJ4QkwrEql5oTtV7PHiDsl0XwkaCWd18o+u625OT7ernmp5mcOJFoigzmLKgih86yDf46PwQSRWSX5Oex2bP58UHkRLhHiuU6kqzDv5DbIcQbqLS5AwhQ0os75BawFSmp0MgCknkBNl5FdxOHj4zyNF7QOvD4Eeyyg0+vkDZr3PDGPbzhApDILnfdirftZ7B95FBAyAYr19BQ+4pUCq0dIPL0QkL+qNvYDgYgPwOox+bnFc5y25gFWWOPB6+ZKLndvUWJ5uIpOemMZZUatCzzK/g/tLbSiioynkZYdq2017MWbmq5F7JoORa3e33p1/gIknsDuD0RTejghUeeGWpcbnuuVqR66TA/Ao+8Ea/YRZG2g72E2SqhWJtbejYVWRi3DX70etDcCL83YyWIL5o5y21WZf2aU4YkkCqWmkr/wrtjIPDT/3RG54ngxcN25ujWmAt08zFoXZ3EjzO9Clpsl2ZNfAcYmbhlqBUjmEyAwLN7gvldGMYV4f5VAF9jaMzsitdiAtW3YTrvO9eETFH8H4e8DDU4X4N0z5kLakd5XdqriBzCmSynH+1Nmg==

I don't understand what you mean, perhaps you could show some example code which does something you didn't expect or want?

Gaëtan Gilbert

On 22/04/2020 17:08, richard Dapoigny wrote:

Dear Coq Members,
We are using the Coq hierarchy of polymorphic universes which has been recently implemented by Sozeau.
We want to use it for subtyping and we expect it to be an implementation of Grothendieck universes, however it seems to be a total order. Therefore we cannot have a tree-like hierarchy.
However is it possible to ultimately have that structure?
Thanks for your answer,
Richard

--
*Richard Dapoigny*
/Associate Professor/ - LISTIC Laboratory
University Savoie Mont-Blanc
5, chemin de Bellevue
Po. Box 80439
Annecy-le-Vieux 74940
FRANCE
https://www.listic.univ-smb.fr/en/presentation-en/members/lecturers/richard-dapoigny-en/

/****** People who don't know history are condemned to repeat it. ******/

[Coq-Club] Question about Coq universes, richard Dapoigny, 04/22/2020
- Re: [Coq-Club] Question about Coq universes, Gaëtan Gilbert, 04/22/2020
  - Re: [Coq-Club] Question about Coq universes, richard Dapoigny, 04/22/2020
    - Re: [Coq-Club] Question about Coq universes, Kenji Maillard, 04/22/2020
      - Re: [Coq-Club] Question about Coq universes, Gaëtan Gilbert, 04/22/2020
        
        Re: [Coq-Club] Question about Coq universes, richard Dapoigny, 04/22/2020
    - Re: [Coq-Club] Question about Coq universes, Pierre Courtieu, 04/22/2020