The Coq mailing list

[Kenji Maillard <chocobodralliam AT gmail.com>]

Hi Richard,

What do you want to achieve exactly ?

I don't think it is exact to say Coq's universe levels form a total order: at any point of a Coq development the universes together with their constraints form a finite graph without any cycle containing a strict edge (<). However you could always map such a graph to a total order by adding more constraints.

In your example, you can see by printings universes that (test t2) adds a constraint sf1 <= sf0 (at least if you add a `Definition x := test t2.`) so that your universe graph is not a tree anymore (and I don't think that there is any way to declare to coq that two universe levels should be incomparable).

Cheers,

Kenji

Le 22/04/2020 à 17:27, richard Dapoigny a écrit :

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