Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Question about Coq universes

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Question about Coq universes


Chronological Thread 
  • 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. ******/




Archive powered by MHonArc 2.6.18.

Top of Page