The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

>I don't think that there is any way to declare to coq that two 
universe levels should be incomparable

You can enforce that a definition produces no new constraints, for instance

~~~coq
Universes sf2 sf1 sf0.
Constraint sf0 < sf2.
Constraint sf1 < sf2.

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

Parameter test : Type@{sf0} -> Prop.
Fail Definition foo@{|} := test t2.
(* universe constraints are not implied by the ones declared *)
~~~

Gaëtan Gilbert

On 22/04/2020 18:00, Kenji Maillard wrote:
> 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. ******/