coq - 什么是 COQ 中的 Set

Question

我仍然不明白是什么类型的套装在 COQ 中的意思。我什么时候使用 套装我什么时候使用 类型 ?

在霍特 套装被定义为一种类型，其中身份证明是唯一的。
但我认为在 Coq 中它有不同的解释。

Answer 1

Set在 Coq 和 HoTT 中意味着完全不同的东西。

在 Coq 中，每个对象都有一个类型，包括类型本身。类型的类型通常被称为排序、种类或宇宙。在 Coq 中，(计算相关的)宇宙是 Set , 和 Type_i ，其中 i范围超过自然数(0, 1, 2, 3, ...)。我们有以下内含物:

Set <= Type_0 <= Type_1 <= Type_2 <= ...

这些 Universe 的类型如下:

 Set : Type_i     for any i

Type_i : Type_j  for any i < j

就像在 Hott 中一样，需要这种分层以确保逻辑一致性。正如安塔尔指出的那样， Set行为大多像最小的 Type ，但有一个异常(exception):当您调用 coqtop 时，它可能会变成不可预测的。与 -impredicative-set选项。具体来说，这意味着 forall X : Set, A类型为 Set每当 A是。相比之下， forall X : Type_i, A类型为 Type_(i + 1) ，即使 A有类型 Type_i .

这种差异的原因是，由于逻辑悖论，只有这种层次结构的最低级别才能成为不可预测的。然后你可能想知道为什么 Set默认情况下不会成为阻碍性的。这是因为一个不可预测的 Set与排中公理的强形式不一致:

forall P : Prop, {P} + {~ P}.

这个公理允许你做的是编写可以决定任意命题的函数。请注意 {P} + {~ P}类型住在 Set ，而不是 Prop .排中的通常形式， forall P : Prop, P \/ ~ P , 不能以同样的方式使用，因为生活在 Prop 中的东西不能以计算相关的方式使用。