Ответ 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, не могут быть использованы соответствующим образом.