coq - 如何在 Coq 中证明 "Type <> Set"(即 Type 不等于 Set)？

Question

Type之间是否存在相等或不等关系？和 Set在 Coq 中？

我正在学习 Coq 的类型系统并了解 Set 的类型是Type@{Set+1} ，以及 Type@{k} 的类型是Type@{k+1} .我试图证明 Type = Set , 然后试图证明 Type <> Set ，但我在这两种情况下都失败了。

我开始了

Lemma set_is_type :  Type = Set.
Proof.
reflexivity.

它给出一条错误消息，指出无法将“Set”与“Type@{Top.74}”统一。

然后我试了一下

Lemma set_is_not_type : Type <> Set.
Proof.
intros contra.

此时我不知道如何进行。攻略discriminate没用，也没有inversion contra .

可以证明以上两个引理中的哪一个？

Answer 1

这实际上不是一个完全微不足道的定理。要证明 Type = Set 会导致悖论(因此必须有不同级别的 Type)，您需要使用类似于罗素悖论的标准结果从集合论。具体来说，您需要 Hurken's paradox ，这实质上是说较小的 Type 不能与较大的 Type 处于同等地位(记住 Type 在 Coq 中是多态的，并且特别是，Set 是最低级别(如果包含 Prop，则为第二低级别)。

我们想要的特定定理可以在标准库中找到。

Require Logic.Hurkens.
Import Logic.Hurkens.TypeNeqSmallType.

Check paradox.

paradox 具有类型签名forall A : Type, Type = A -> False。这正是我们想要证明的，因为 Set: Type(至少如果 Type 足够大)。

Lemma set_is_not_type: Type <> Set.
Proof.
  intro F.
  exact (paradox _ F).
Defined.

Coq 自动对这个引理中的 Type 设置限制，以确保 Set: Type。

---

另一方面，Set 等于Type 的some 层，所以我们应该能够证明Type = 设置 对此 Type 有一些不同的约束。我发现最简单的方法是证明 Type = Type，然后用 Set 实例化这个定理。无论出于何种原因，正如您发现的那样，反身性本身无法强制执行宇宙约束。为此，我们需要使引理宇宙成为多态的，以便它们可以用特定的宇宙级别实例化。

Polymorphic Lemma type_is_type: Type = Type.
Proof.
  reflexivity.
Defined.

Polymorphic Lemma type_is_set: Type = Set.
Proof.
  apply type_is_type.
Defined.

让一切 Universe 多态化的更简单方法是将 Set Universe Polymorphism. 放在一切之前。