COQ中的Set究竟是什么

Question

我仍然对COQ中排序Set的含义感到困惑.我何时使用Set,何时使用Type？

在Hott中,Set被定义为一种类型,其中身份证明是唯一的.但我认为在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,但有一个例外:它可以制成impredicative当你调用coqtop与-impredicative-set选择.具体地说,这意味着什么时候都是forall X : Set, A类型.相比之下,即使有类型,也属于类型.SetAforall X : Type_i, AType_(i + 1)AType_i

这种差异的原因在于,由于逻辑悖论,只有这种层次结构的最低级别才能产生不可预测性.然后你可能想知道为什么Set默认情况下不会产生不可预测性.这是因为一种不可预测Set的与被排斥中间的公理的强烈形式不一致:

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

这个公理允许你做的是编写可以决定任意命题的函数.请注意,该{P} + {~ P}类型存在于Set,而不是Prop.排中的一般形式,forall P : Prop, P \/ ~ P不能以同样的方式使用,因为事情住在Prop不能在计算相关的方式来使用.

Answer 2

除了亚瑟的回答之外：

\n\n

Set从位于层次结构底部的 事实来看，

\n\n

\n

随之而来的Set是 \xe2\x80\x9csmall\xe2\x80\x9d 数据类型和函数类型的类型，即其值不直接或间接涉及类型的类型。

\n

\n\n

这意味着以下操作将失败：

\n\n

Fail Inductive Ts  : Set :=\n  | constrS : Set -> Ts.\n

\n\n

出现此错误消息：

\n\n

\n

大型非命题归纳类型必须位于 中Type。

\n

\n\n

正如消息所示，我们可以使用以下方法修改它Type：

\n\n

Inductive Tt : Type :=\n  | constrT : Set -> Tt.\n

\n\n

参考：

\n\n

\n
• 《Coq 作为形式系统的本质》B. Jacobs (2013)，pdf。
\n

\n