宇宙不一致的一个简单案例

Question

我可以定义以下归纳类型：

Inductive T : Type -> Type :=
| c1 : forall (A : Type), A -> T A
| c2 : T unit.

但随后命令 Check (c1 (T nat)) 失败并显示以下消息：术语 T nat 的类型为 Type@{max(Set, Top.3+1)}，而预期的类型为 Type@{Top.3}（宇宙不一致）。

如何调整上述归纳定义，使c1 (T nat) 不会导致宇宙不一致，并且不设置宇宙多态性？

以下有效，但我更喜欢不添加相等性的解决方案：

Inductive T (A : Type) : Type :=
| c1 : A -> T A
| c2' : A = unit -> T A.

Definition c2 : T unit := c2' unit eq_refl.

Check (c1 (T nat)).
(*
c1 (T nat)
     : T nat -> T (T nat)
*)

Answer 1

让我首先回答为什么我们首先会得到宇宙不一致的问题。

Universe inconsistencies 是 Coq 报告的错误，以避免通过 Russell 悖论证明 False，这是由于考虑了所有不包含自身的集合的集合。

在类型论中有一个更方便形式化的变体，称为 Hurken 悖论；有关详细信息，请参阅Coq.Logic.Hurkens。 Hurken 悖论有一个特殊化，它证明没有类型可以缩回到更小的类型。也就是说，给定

U := Type@{u}
A : U
down : U -> A
up : A -> U
up_down : forall (X:U), up (down X) = X

我们可以证明False。

---

这几乎就是您的Inductive 类型的设置。用宇宙注释你的类型，你从

开始

Inductive T : Type@{i} -> Type@{j} :=
| c1 : forall (A : Type@{i}), A -> T A
| c2 : T unit.

请注意，我们可以反转这个归纳；我们可以写

Definition c1' (A : Type@{i}) (v : T A) : A
  := match v with
     | c1 A x => x
     | c2 => tt
     end.

Lemma c1'_c1 (A : Type@{i}) : forall v, c1' A (c1 A v) = v.
Proof. reflexivity. Qed.

暂时假设c1 (T nat) 进行了类型检查。由于T nat : Type@{j}，这将需要j <= i。如果它给了我们j < i，那么我们将被设置。我们可以写c1 Type@{j}。这正是我上面提到的 Hurken 变体的设置！我们可以定义

u = j
U := Type@{j}
A := T Type@{j}
down : U -> A := c1 Type@{j}
up : A -> U := c1' Type@{j}
up_down := c1'_c1 Type@{j}

因此证明False。

Coq 需要实现一个规则来避免这个悖论。如here 所述，规则是对于归纳的构造函数的每个（非参数）参数，如果参数的类型在全域u 中具有排序，则归纳的全域被约束为>= u。在这种情况下，这比 Coq 需要的更严格。正如 SkySkimmer here 所提到的，Coq 可以识别直接出现在作为归纳索引的位置的参数，并以与忽略参数相同的方式忽略这些参数。

---

所以，要最终回答您的问题，我相信以下是您唯一的选择：

1. 您可以Set Universe Polymorphism 以便在T (T nat) 中，您的两个Ts 采用不同的宇宙参数。 （等效地，你可以写Polymorphic Inductive。）
2. 您可以利用 Coq 如何专门处理归纳类型的参数，这要求在您的情况下使用相等。 （使用相等性的要求是从索引归纳类型到参数化归纳类型的一般属性——从将参数从 : 之后移动到它之前。）
3. 您可以将标志 -type-in-type 传递给 Coq，以完全禁用 Universe 检查。
4. 您可以fix bug #7929（我在深入研究这个问题时报告过）让 Coq 处理出现在归纳中索引位置的构造函数的参数，就像它处理归纳类型的参数一样。
5. （您可以找到系统的另一个边缘案例，并设法欺骗 Coq 忽略您想要绕过它的宇宙，并可能在此过程中找到 False 的证明。（可能涉及模块子类型化，请参阅，例如，this recent bug in modules with universes.))