究竟是一套在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。