Coq中Type和Set之间是否存在相等或不平等关系？
我正在学习Coq的类型系统，并了解Set的类型是Type@{Set+1}，并且Type@{k}的类型是Type@{k+1}。我试图证明Type = Set，然后试图证明Type <> Set，但我在这两种情况下都失败了。
我从
Lemma set_is_type : Type = Set.
Proof.
reflexivity.
它给出一条错误消息，指出无法将">设置"与"Type@{Top.74}"统一。
然后我试了
Lemma set_is_not_type : Type <> Set.
Proof.
intros contra.
在这一点上，我不知道如何进行。战术discriminate不起作用，也没有inversion contra.
以上两个引理中哪一个可以证明？
这实际上不是一个完全微不足道的定理。为了证明Type = Set导致悖论(因此需要具有单独的Type水平)，您需要使用类似于集合论中的罗素悖论的标准结果。具体来说，你需要 Hurken 悖论，它本质上是说较小的Type不能与较大的Types 处于同等地位(请记住，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，所以我们应该能够证明Type = Set对这个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.
使万物宇宙多态的更简单方法是把Set Universe Polymorphism.放在万物之前。