coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Question about Coq universes

From: richard Dapoigny <richard.dapoigny AT univ-smb.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] Question about Coq universes
Date: Wed, 22 Apr 2020 17:08:06 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=richard.dapoigny AT univ-smb.fr; spf=Pass smtp.mailfrom=richard.dapoigny AT univ-smb.fr; spf=None smtp.helo=postmaster AT smtpout02-ext3.partage.renater.fr

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