Давайте теперь притворимся, что код HoTT использует A -> Prop вместо A -> Type; разница между ними ортогональна вашему вопросу.
Параметризованное суждение P : A -> Prop является просто свойством элементов типа A. Помимо простого предложения is_three, описанного выше, мы можем выразить более сложные свойства натуральных чисел таким способом. Например:
Definition even (n : nat) : Prop :=
exists p, n = 2 * p.
Definition prime (n : nat) : Prop :=
n >= 2 /\
forall p q, n = p * q -> p = n \/ p = 1.
Тип type sigT A P позволяет нам ограничить тип A элементами, которые удовлетворяют свойству P. Например, sigT nat even - это тип всех четных чисел, sigT nat prime - это тип всех простых чисел и т. Д. В Coq свойства являются более примитивным понятием, а типы подмножеств, такие как sigT, являются производным понятием.
В традиционной математике понятия свойства и подмножества можно почти сопоставить: говорить, что 2 - простое число, равносильно тому, что оно принадлежит множеству всех простых чисел. В теории типов Кока это не совсем так, потому что элемент типа является , а не суждением: вы, например, не можете сформулировать теорему о том, что 2 является элементом sigT nat prime. Следующий фрагмент кода выдает ошибку:
Lemma bogus : (2 : {x : nat & prime x}).
(* Error: *)
(* The term "2" has type "nat" while it is expected to have type *)
(* "{x : nat & prime x}". *)
({ ... & ... } - синтаксический сахар для типа sigT, определенного в стандартной библиотеке Coq.)
Самое близкое, что мы можем получить, это сказать, что 2 можно извлечь из этого типа:
Lemma fixed : exists x : {x : nat & prime x}, 2 = projT1 x.
где projT1 - это функция, которая извлекает первый компонент зависимой пары. Однако это гораздо более громоздко, чем просто указывать, что 2 простое число:
Lemma prime_two : prime 2.
Как правило, параметризованные предложения более полезны в Coq, но есть случаи, когда тип sigT пригодится; например, когда мы заботимся только об элементах типа, которые удовлетворяют определенному свойству. Представьте, что вы реализуете ассоциативную карту в Coq, используя тип бинарных деревьев поиска. Вы можете начать с определения типа tree из произвольных деревьев:
Inductive tree :
| Leaf : tree
| Node : tree -> nat -> nat -> tree -> tree.
Этот тип определяет двоичное дерево, в узлах которого хранится пара ключ-значение натуральных чисел. Чтобы реализовать функции для поиска элемента, обновления значения и т. Д., Используя этот тип, мы могли бы поддерживать инвариант сортировки ключей дерева (то есть, что ключи в левом поддереве меньше, чем ключи узел, и наоборот для правого поддерева). Поскольку пользователи этого дерева не захотят рассматривать деревья, которые не удовлетворяют этому инварианту, мы могли бы вместо этого использовать тип sigT tree well_formed, где well_formed : tree -> Prop выражает вышеуказанный инвариант. Основное преимущество заключается в том, что это упрощает интерфейс нашей библиотеки: вместо отдельной леммы о том, что функция вставки сохраняет инвариант, это автоматически выражается в типе самой функции вставки; пользователям даже не нужно беспокоиться о том, что деревья, которые они строят с использованием интерфейса, уважают инвариант.
Что касается вашего второго вопроса, равенство настолько фундаментально, что без него сложно определить интересные свойства. Например, свойства even и prime выше определены как равенство.