coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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, Gaëtan Gilbert, 04/22/2020
- Re: [Coq-Club] Question about Coq universes, Pierre Courtieu, 04/22/2020
- Re: [Coq-Club] Question about Coq universes, Kenji Maillard, 04/22/2020
- Re: [Coq-Club] Question about Coq universes, richard Dapoigny, 04/22/2020
- Re: [Coq-Club] Question about Coq universes, Gaëtan Gilbert, 04/22/2020
Archive powered by MHonArc 2.6.18.