2018-06-09

Встраивание MLTT в тайп чекер

Стрим на мокуме начинается с "Конструктивного доказательства унивалентности", теоремы которая стала возможной только в августе 2017 года! Я думаю надо понижать планку и рассказать вам о первой лекции, которую я всегда даю по завтиповой теории. В этой лекции мы формально выписываем все формейшин рулы, интродакшин рулы, элиминейшин рулы и бета и эта равенства для трех типов, из которых состоит MLTT: Пи, Сигма и Равенство. И что интересно, если записать MLTT на самой MLTT то, получится, что доказательство большинства равенств будет состоять из reflection интродакшин рула от типа равенства. Таким образом показывается, что NBE настолько мощная штука, что может доказать почти все теоремы MLTT, кроме компютейшинал правила (эта-правило) для равенства. Я засекал на видосе live-кодинг и формального доказательства всей MLTT в кубике у меня уместилось в пару часов. В качестве пейпера который можно взять как основу для данной демонстрации я беру Мартина Хоффмана и Томаса Страйхера "Групоидная интерпретация теории типов", работы, с которой начался путь в унивалентные основания. Но вообще можно брать любой пейпер по MLTT начиная с Мартина-Лёфа 1984.


\import Pi
\import Sigma
\import Path

\record MLTT
  (A : \Type)
  (Pi_Former : \Pi (A -> \Type) -> \Type)
  (Pi_Intro : \Pi (B : A -> \Type) -> Pi A B -> Pi A B)
  (Pi_Elim : \Pi (B : A -> \Type) -> Pi A B -> Pi A B)
  (Pi_Comp1 : \Pi (B : A -> \Type) (f : Pi A B) (a : A)
    -> Path (B a) (Pi_Elim B (Pi_Intro B f) a) (f a))
  (Pi_Comp2 : \Pi (B : A -> \Type) (f : Pi A B)
    -> Path (Pi A B) f (Pi_Intro B f))
  (Sigma_Former : \Pi (A -> \Type) -> \Type)
  (Sigma_Intro : \Pi (B : A -> \Type) (a : A) (b : B a) -> Sigma A B)
  (Sigma_Elim1 : \Pi (B : A -> \Type) (x : Sigma A B) -> A)
  (Sigma_Elim2 : \Pi (B : A -> \Type) (x : Sigma A B) -> B (pi1 A B x))
  (Sigma_Comp1 : \Pi (B : A -> \Type) (a : A) (b : B a)
    -> a = (Sigma_Elim1 B (Sigma_Intro B a b)))
  (Sigma_Comp2 : \Pi (B : A -> \Type) (a : A) (b : B a)
    -> b = (Sigma_Elim2 B (a,b)))
  (Sigma_Comp3 : \Pi (B : A -> \Type) (p : Sigma A B)
    -> p = Sigma_Intro B (pi1 A B p) (Sigma_Elim2 B p))
  (Id_Former : A -> A -> \Type)
  (Id_Intro : \Pi (a : A) -> Path A a a)
  (Id_Elim : \Pi (a : A) (C : \Pi (x : A) -> a = x -> \Type)
    (d : C a (refl A a)) (x : A) (p : a = x) -> C x p)


 \func check (A : \Type) : MLTT
   => \new MLTT A (Pi A) (lam A) (app A) (beta A) (eta A)
                  (Sigma A) (dpair A) (pi1 A) (pi2 A) (beta1 A) (beta2 A) (eta2 A)
                  (Path A) (refl A) (J A)

[1]. https://github.com/groupoid/cubical/blob/master/src/mltt.ctt
[2]. https://www.youtube.com/watch?v=JsHminiPzzs
[3]. M.Sokhatskyi. Issue I: Internalizing Martin-Löf Type Theory