Что такое Set в COQ

Я все еще озадачен тем, что означает Установить в COQ. Когда я использую Установить и когда я использую Тип?

В Hott Установить определяется как тип, где доказательства идентичности уникальны. Но я думаю, что в Кок есть другая интерпретация.

Ответ 1

Set означает довольно разные вещи в Coq и HoTT.

В Coq каждый объект имеет тип, включая сами типы. Типы типов обычно называются сортами, видами или юниверсами. В Coq все (все релевантно вычислимые) вселенные Set и Type_i, где i пробегает натуральные числа (0, 1, 2, 3,...). Имеются следующие включения:

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

Эти юниверсы печатаются следующим образом:

 Set : Type_i     for any i

Type_i : Type_j  for any i < j

Как и в Hott, эта стратификация необходима для обеспечения логической последовательности. Как отметил Антал, Set ведет себя в основном как наименьший Type, за одним исключением: его можно сделать нечистым, когда вы вызываете 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, не могут быть использованы соответствующим образом.

Ответ 2

В дополнение к ответу Артура:

Из того факта, что Set расположен в нижней части иерархии,

из этого следует, что Set - это тип "малых" типов данных и типов функций, т.е. тех, чьи значения прямо или косвенно не включают типы.

Это означает, что следующее не удастся:

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

с этим сообщением об ошибке:

Большие непропозициональные индуктивные типы должны быть в Type.

Как следует из сообщения, мы можем изменить его, используя Type:

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

Ссылка:

Сущность Coq как формальной системы. Б. Джейкобс (2013), pdf.