究竟是一套在COQ

Question

我仍然困惑什么那种设置意味着在COQ。我何时使用Set以及何时使用类型？

In Hott a 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，需要这种分层，以确保逻辑一致性。 As Antal指出，Set的行为大多像最小的Type，但有一个例外：当您使用-impredicative-set选项调用coqtop时，可以将其作为impregnicative。具体而言，这意味着forall X : Set, A的类型是Set，只要A是。相反，forall X : Type_i, A类型为Type_(i + 1)，即使当A具有类型Type_i时也是如此。

造成这种差异的原因是，由于逻辑上的矛盾，只有这样的层次结构的最低级别可以被认为是不可预测的。那么你可能会想知道为什么Set默认情况下没有被预测到。这是因为impredicative Set与排中的公理的强式不一致：

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

什么这个公理允许你做的是编写一个可以决定任意命题功能。请注意，​​类型生活在Set中，而不是Prop。排除中间的通常形式forall P : Prop, P \/ ~ P不能以相同的方式使用，因为生活在Prop中的事物不能以计算相关的方式使用。

Answer 2

除了亚瑟的答案：

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

接下去Set是“小”的数据类型和函数类型的类型即那些其值不直接或间接涉及类型的那些。

这意味着以下将失败：

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

与此错误消息：

大的非命题归纳类型必须是Type。

作为消息表明，我们可以通过使用Type修改它：

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

参考：

• 勒柯克的本质由B. Jacobs的一个形式系统（2013）， pdf。