Coq 中的 Set 到底是什么
What exactly is a Set in Coq
我仍然不明白 sort Set 在 Coq 中的含义。什么时候使用 Set 什么时候使用 Type?
在 Hott 中，集合 被定义为一种类型，其中身份证明是唯一的。
但我认为在 Coq 中它有不同的解释。
Set 在 Coq 和 HoTT 中的意思完全不同。
在 Coq 中，每个对象都有一个类型，包括类型本身。类型的类型通常称为 sorts、kinds 或 universes。在 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
就像霍特一样，需要这种分层来确保逻辑的一致性。正如 Antal 指出的那样，Set 的行为大部分类似于最小的 Type，但有一个例外：当您使用-impredicative-set 选项。具体来说，这意味着只要 A 是，forall X : Set, A 就是 Set 类型。相反，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 中的东西不能以计算相关的方式使用。
除了亚瑟的回答：
从 Set 位于层次结构底部的事实来看，
it follows that Set is the type of the “small” datatypes and function types, i.e. the ones whose values do not directly or indirectly involve types.
这意味着以下操作将失败：
Fail Inductive Ts : Set :=
| constrS : Set -> Ts.
出现此错误消息：
Large non-propositional inductive types must be in Type.
根据消息提示，我们可以修改为Type:
Inductive Tt : Type :=
| constrT : Set -> Tt.
参考：
- B. Jacobs (2013) 的《Coq 作为正式系统的本质》，pdf。
我仍然不明白 sort Set 在 Coq 中的含义。什么时候使用 Set 什么时候使用 Type?
在 Hott 中，集合 被定义为一种类型，其中身份证明是唯一的。 但我认为在 Coq 中它有不同的解释。
Set 在 Coq 和 HoTT 中的意思完全不同。
在 Coq 中，每个对象都有一个类型，包括类型本身。类型的类型通常称为 sorts、kinds 或 universes。在 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
就像霍特一样，需要这种分层来确保逻辑的一致性。正如 Antal 指出的那样，Set 的行为大部分类似于最小的 Type，但有一个例外：当您使用-impredicative-set 选项。具体来说，这意味着只要 A 是，forall X : Set, A 就是 Set 类型。相反，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 中的东西不能以计算相关的方式使用。
除了亚瑟的回答：
从 Set 位于层次结构底部的事实来看，
it follows that
Setis the type of the “small” datatypes and function types, i.e. the ones whose values do not directly or indirectly involve types.
这意味着以下操作将失败：
Fail Inductive Ts : Set :=
| constrS : Set -> Ts.
出现此错误消息：
Large non-propositional inductive types must be in
Type.
根据消息提示，我们可以修改为Type:
Inductive Tt : Type :=
| constrT : Set -> Tt.
参考：
- B. Jacobs (2013) 的《Coq 作为正式系统的本质》，pdf。