The Coq mailing list

[richard Dapoigny <richard.dapoigny AT univ-smb.fr>]

Thanks for your prompt answer. Let us consider the following test :

Universes sf2 sf1 sf0.
Constraint sf0 < sf2.
Constraint sf1 < sf2.

Parameter t1 : Type@{sf0}.
Parameter t2 : Type@{sf1}.

Parameter test : Type@{sf0} -> Prop.
Check (test t1).
(* we expect that sf0 and sf1 are two branches under sf2 and that the following test fails *)
Check (test t2).

Le 22/04/2020 à 17:12, Gaëtan Gilbert a écrit :

    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. ******/
>         
>         
>

--
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. ******