Типом типа является юниверс.Обычно вселенные стратифицируются на уровни, такие как Тип 0, Тип 1, Тип 2 ..., где типом Типа является Тип (n + 1).Причина этого заключается в том, что если бы у нас был только один уровень типа, типом типа должен был бы быть тип, который часто приводит к парадоксам .
Так что же является типом * 1005?* (тип пи с использованием синтаксиса Coq)?Если мы предположим, что A: Type m и P: A -> Type n, мы имеем forall a: A, P a: Type max(m, n).Если у нас есть совокупные вселенные (как у Coq), так что m≤n и A: Type m подразумевают A: Type n, то на самом деле тип forall a: A, P a - это любая вселенная, которая больше, чем m и n.
EDIT: в ответ на ваш комментарий -> принимает в качестве аргументов A: Type m и P: A -> Type n и возвращает forall a: A, P a, тип которого Type max(m, n), поэтому тип конструктора pi равен forall (A: Type m) (P: A -> Type n), Type max(m, n),или, в синтаксисе Агды, (A: Set m) (P: A -> Set n) -> Set max(m, n).