The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hi,

As far as I understand the constraints you express do not prevent sf1 and sf0 to be equal. When you introduce constraints Coq consider them as the "minimal" ones that must hold, but nothing prevents the typer from adding new relations if they don't break the order relation. Here adding sf1=sf0 (or sf1<=sf0 or sf0<=sf1) does not break the constraints. As you can check:

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

I don't think there is a way to say sf0 <> sf1 without saying either sf1>sf0 or sf0 > sf1.

So as far as I understand the correct statement is: given the constraints Coq checks the existence of a total (weak) ordering (>=) and its associated strict ordering which satisfies the constraints. In particular I don't think there is no way in coq to force (u <> v) without forcing either u>v or v>u. 

You can see this by adding a definition wich forces the sf1=sf0:

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

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

Parameter test : Type@{sf0} -> Prop.
Print Universes Subgraph(sf1 sf2 sf0).
Check (test t1).
Check (test t2).
Print Universes Subgraph(sf1 sf2 sf0).
Definition foo := test t2.

P.

Le mer. 22 avr. 2020 à 17:26, richard Dapoigny <richard.dapoigny AT univ-smb.fr> 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. ******