types - Coq:带有显式 Universe 的固定 Universe 层次结构

Question

我正在研究使用 explicit universes 的可能性用于在 Coq 中构建固定的 Universe 层次结构。在构建它时使用常量 (2, 3, 4) 的尝试失败了:最后，所有组合仍然类型检查(即所有声明的宇宙都被视为分层任意):

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.

请注意 Definition k := Type@{2}和 Definition k := Type@{x+1}导致语法错误。是否可以使用显式 Universe 来构建固定的层次结构，如果可以，如何使用？

Answer 1

我让它工作的方式如下:

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

(但也许比我更有见识的人会提出更好的想法？特别是，这种方法不允许声明固定常量，因此在声明的级别之间可能仍然存在任意多个级别。)