Coq: fixed universe hierarchy w/ explicit universes

Question

I'm looking into the possibility of using explicit universes for building a fixed universe hierarchy in Coq. The attempt to use constants (2, 3, 4) in building it failed: at the end, all combinations still typecheck (i.e. all declared universes are treated 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} result in a syntax error. Is it possible to use explicit universes for building a fixed hierarchy and if so, how?

Answer 1

The way I've gotten it to work is as follows:

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

(But maybe someone more knowledgeable than me will chime in with better ideas? In particular, this approach doesn't allow to declare fixed constants so there may still be arbitrary many levels in between declared levels.)