Иерархия типов в Agda

А почему бы не спросить саму Агду? Я собираюсь использовать отличный режим Agda для Emacs. Начнем с:

module Hierarchy where

postulate
  X : Set

data Y : X → Set where
  -- empty

Мы должны загрузить файл, используя C-c C-l; этот тип проверяет файл, превращает ? в дыры, выделяет синтаксис и так далее.

Теперь есть команда "Infer (deduce) type", доступная через C-c C-d, поэтому давайте воспользуемся этим:

> C-c C-d
Expression:
> Y
X → Set

Верно, в этом есть смысл. Мы определили Y : X → Set, так что это не должно вызывать удивления. Спросим еще раз:

> C-c C-d
Expression:
> X → Set
Set₁

Итак, вот оно: Y : X → Set : Set₁.

Хотя первая часть отвечает на вопрос и показывает, как это проверить самостоятельно, делать это каждый раз было бы, по крайней мере, скучно. Вот как это работает:

Чтобы избежать парадоксов, мы требуем

Set i : Set (i + 1)

что дает вам (бесконечную) иерархию Sets. Если бы у вас был Set : Set (который Agda разрешает с помощью флага --type-in-type), вы могли бы получить противоречие, например этот.

Это также дает нам простое правило для функций:

A : Set i
B : A → Set j

(a : A) → B a : Set (max i j)

Применяя это к вашему примеру:

X   : Set
Set : Set₁

X → Set : Set (max 0 1)
X → Set : Set₁