Coq：使用明确的宇宙层次结构修复了宇宙问题。

Question

我正在研究在Coq中使用显式宇宙构建一个固定的宇宙层次结构的可能性。尝试使用常量（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} 会导致语法错误。是否可以使用显式宇宙来构建一个固定的层次结构，如果可以，如何实现？

- jaam

---

允许的确切宇宙表达式包括：Set（0），变量，变量+1和max()。请参见https://coq.inria.fr/refman/language/core/sorts.html末尾附近的内容。 - lephe

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

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

- nobody

Answer 2

可以使用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.

请注意，这种方法实际上并没有很好地解决宇宙级别的问题。

- Anton Trunov

---

显然，这就是应该完成的方式。我怀疑无法修复已声明宇宙变量的级别。 - jaam

我认为你是正确的。虽然我没有查看源代码，但从我读过的论文中可以得出结论，宇宙级别不存在显式数字，只有抽象变量之间的约束关系。不过，我可能是错的。如果您想确保，最好询问Coq俱乐部邮件列表。 - Anton Trunov

Answer 3

你可以使用公理来规定一个固定的宇宙层次结构：

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.

没有人提出的问题仍然是一个未解决的挑战。

- jaam