Что такое Set в COQ

Question

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

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

Answer 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, за одним исключением: его можно сделать impredicative, когда вы вызываете 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, не могут быть использованы соответствующим образом.

Answer 2

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

Из того, что Set находится в нижней части иерархии,

следует, что Set является тип «малых» типов данных и типов функций , т. е. те, чьи значения прямо или косвенно не связаны с типами.

Это означает, что следующий будет терпеть неудачу:

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

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

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

В сообщении предложить, мы можем изменить его с помощью Type:

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

Ссылка:

• Сущность Coq как формальная система Б. Jacobs (2013 г.), pdf.