Coq: fixed universe hierarchy with explicit universes

Question

I am exploring the possibility of using explicit universesCoq to create a fixed hierarchy of universes. An attempt to use constants (2, 3, 4) when creating it failed: in the end, all combinations are still of type (i.e., all declared universes are considered as hierarchically arbitrary):

Universe k l m x y z.
Let x := 2.
Definition k := Type@{x}.
Notation y := 3.
Definition l := Type@{y}.
Notation z := 4.
Definition m := Type@{z}.
Print x. (*x = 2: nat*)
Print y. (*Notation y := 3*)
Check l:k:m.
Check m:k:l.
Check k:m:l.

Note that Definition k := Type@{2}and Definition k := Type@{x+1}lead to a syntax error. Can explicit universes be used to build a fixed hierarchy, and if so, how?

Answer 1

You can use the command Constraint:

Universes x y z.

Constraint x < y, y < z.

Definition X := Type@{x}.
Definition Y := Type@{y}.
Definition Z := Type@{z}.

Check X:Y.
Check Y:Z.
Check X:Z.
Fail Check Z:Y.
Fail Check Y:X.
Fail Check Z:X.

Note that this approach does not really set universe levels.

Answer 2

:

Universe X Y Z.
Definition x := Type@{X}.
Definition y := Type@{Y}.
Definition z := Type@{Z}.

(* bogus definition to fix hierarchy *)
Definition dummy:x:y:z := unit.

Check x:y.
(* ok:
   x : y
        : y
*)

Check x:z.
(* also ok (transitivity is still acceptable):
   x : z
        : z
*)

Check z:y.
(* Error:
   The term "z" has type "Type@{Z+1}" while it is expected to have type "y"
   (universe inconsistency: Cannot enforce Z < Y because Y < Z).
*)

( , - , , ? , , .)

Answer 3

You can specify a fixed universe hierarchy with an axiom:

Universe X Y Z.
Notation X := Type@{X}.
Notation Y := Type@{Y}.
Definition Z := Type@{Z}.
Axiom fuh: (fun (x:Type) => x)(X:Y:Z).
Check X:Y.
Check Y:Z.
Check X:Z.
Fail Check Z:Y.
Fail Check Y:X.
Fail Check Z:X.

The particular challenge facing anyone remains an open challenge