Я все еще пытаюсь внедрить теорию типов наблюдений в себя и все это в Агду.

В настоящее время у меня есть следующая иерархия вселенных:

Prop : Type 0 : Type 1 : ...
(∀ α -> Type α) : Type ω₀ : Type ω₁

Чтобы определить равенство полиморфных функций вселенной, мне нужно было добавить код для Type ω₀, что заставило меня добавить Type ω₁ в метатеорию. Подробнее об этом в предыдущем вопросе.

Вот основные функции целевой теории, типы которых поднимаются до метатеории оператором интерпретации ⟦_⟧.

mutual
  Eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> univ⁺ α ⇒ univ⁺ β ⇒ prop) ⟧
  eq : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> A ⇒ B ⇒ prop) ⟧

mutual
  coerce : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> Eq _ _ A B ⇒ A ⇒ B) ⟧
  postulate
    coherence : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> 
                     π (Eq _ _ A B) λ r -> π A λ x -> eq _ _ A B x (coerce _ _ A B r x)) ⟧

Это работает таким образом, но я хочу доказать coherence а не постулировать. Возникают две проблемы:

Первое

Как доказать, что одинаковые типы лежат в одной вселенной? Верно ли это (в конструктивном смысле) вообще? Благодаря Конору Макбрайду у нас есть следующий слоган

Теперь я думаю, что a == b означает

как только вы узнаете, что a и b имеют одинаковые типы, вы узнаете, что они имеют одинаковые значения

Но типы — это значения — не означает ли это, что «как только вы узнаете, что A и B лежат в одной вселенной, вы узнаете, что они имеют одинаковые значения»? Спрашиваю, потому что не могу доказать eq x y -> Eq (eq x z) (eq x y) иначе (в статье приводится более общая лемма, но этой достаточно, чтобы получить sym, trans и другие). Проблема заключается в том, что для присвоения типа cong (\z' -> eq z' z) p, где p : eq x y, cong должны принимать полиморфную функцию юниверса, потому что x и y имеют наблюдаемо одинаковые, но по определению разные типы. А так как равенство функций поточечное, то cong требует доказательства равенства вселенных, где лежат типы x и y. В коде это выглядит так:

postulate
  refl : ⟦ (π₁ lev λ α -> π (univ⁺ α) λ A -> π A λ x -> eq _ _ A A x x) ⟧
  cong-levOf : ⟦ (π₀ nat λ α -> π₀ nat λ β ->
                    π (univ α) λ A -> π (univ β) λ B -> Eq _ _ A B ⇒ α ≟ℕ β) ⟧

hsubstitutive : ⟦ (π₀ nat λ α -> π₀ nat λ β -> π₀ nat λ δ ->
                     π (univ α) λ A -> π (univ β) λ B -> π A λ x -> π B λ y ->
                       π (π₀ nat λ γ -> π (univ γ) λ C -> C ⇒ univ δ) λ D ->
                         Eq _ _ A B ⇒ eq _ _ A B x y ⇒ Eq _ _ (D _ A x) (D _ B y)) ⟧
hsubstitutive α β δ A B x y D r q =
  refl _ (π₀ nat λ γ -> π (univ γ) λ C -> C ⇒ univ δ) D _ _ (cong-levOf _ _ A B r) A B r x y q

cong-≅z : ⟦ (π₀ nat λ α -> π₀ nat λ β -> π₀ nat λ γ ->
               π (univ α) λ A -> π (univ β) λ B -> π (univ γ) λ C ->
                 π A λ x -> π B λ y -> π C λ z -> Eq _ _ A B ⇒
                   eq _ _ A B x y ⇒ Eq _ _ (eq _ _ A C x z) (eq _ _ B C y z)) ⟧
cong-≅z α β γ A B C x y z r q = hsubstitutive _ _ _ A B x y (λ _ C' z' -> eq _ _ C' C z' z) r q

Доказательство предоставлено cong-levOf _ _ A B r, где cong-levOf постулируется.

Второй

Тип coherence есть

coherence : ⟦ (π₁ lev λ α -> π₁ lev λ β -> π (univ⁺ α) λ A -> π (univ⁺ β) λ B -> 
                 π (Eq _ _ A B) λ r -> π A λ x -> eq _ _ A B x (coerce _ _ A B r x)) ⟧

но тип, скажем, sym есть

sym : ⟦ (π₀ nat λ α -> π₀ nat λ β -> π (univ α) λ A -> π (univ β) λ B ->
           π A λ x -> π B λ y -> Eq _ _ A B ⇒ eq _ _ A B x y ⇒ eq _ _ B A y x) ⟧

π₀ вместо π₁ везде. Причина этого в том, что тип, переданный в refl в hsubstitutive, является (π₀ nat λ γ -> π (univ γ) λ C -> C ⇒ univ δ) и не может быть (π₁ lev λ γ -> π₁ (univ⁺ γ) λ C -> C ⇒ univ⁺ δ) по мере необходимости, потому что этот тип слишком велик и не имеет типа в целевой теории. Таким образом, мы не можем использовать sym при проверке coherence, потому что он не может обрабатывать достаточно большие типы. То же самое относится и к большинству других комбинаторов, что делает coherence недоказуемым.

Единственное решение, которое я вижу, это добавить Type ω₂ к метатеории и код для Type ω₁ к целевой теории. Тогда типы Eq, eq , refl и cong (имею в виду обычный cong f : eq x y -> eq (f x) (f y) — даже для «маленьких» (ω₁) Eq и eq он должен быть в Type ω₂, потому что f может быть большим) будут лежать в Type ω₂, так что мы можем, например. говорят, что Type ω₀ (но не выше) равно самому себе. А типы coerce и coherence будут лежать в Type ω₁, так что пока мы можем сказать, что Type ω₀ равно самому себе, принудить по этому уравнению не получится (не звучит как большая проблема).

Я думаю, вместо того, чтобы добавлять Type ω₂ в иерархию, проще сделать это

Prop : Type 0 : Type 1 : ...
(∀ α -> Type α) : Type ω₀ : Type ω₁ : Type ω₂ : Type ω₃ : ...

но прежде чем я сойду с ума, не могли бы вы сказать, звучит ли это как хороший план? Я гоняюсь за своим хвостом за последним расширением вселенной Type ω₂?

Я также повторю здесь вопросы из первой части: Как доказать, что одинаковые типы лежат в одной вселенной? Верно ли это (в конструктивном смысле) вообще? Верно ли, что «Уравнение A B означает, что как только вы узнаете, что A и B лежат в одной и той же вселенной, вы узнаете, что они имеют равные значения»?