Кодировка Изоморфизмами

Специально для канала Формальная Философия. В статье не рассматривается ничего сложнее чем encode-decode XML <-> JSON вместе с правилами enc dec = id и dec enc = id. Просто вместо переменных XML/JSON мы рассматриваем несколько конкретных типов: Iso, Equiv, Pi, Interval. Другими словами, мы будем кодировать эти типы и транспорты между ними с помощью изоморфизмамов.

Вступление

Как вы знаете все индуктивные типы (Nat, List и т.д.) могут быть представлены в Чёрч-кодировке которая есть упаковка категорной модели. Идея кодирования следующая, раз мы работаем в теории категорий, то всё сущности мы рассматриваем как объекты и связи между ними (везде одно и то же). Значит и индуктивные типы мы раскладываем в это же, т.е. другими словами мы строим категорную модель конкретных индуктивных инстансов data, или как говорят мы строим категории F-алгебр:

natOb: U = (X: U) * (zero: X) * (succ: X -> X) * unit natHom (x1 x2: natOb): U = (map: x1.1 -> x2.1) * (mapZero: Path x2.1 (map (x1.2.1)) (x2.2.1)) * (mapSucc: (x: x1.1) -> Path x2.1 (map (x1.2.2.1 x)) (x2.2.2.1 (map x))) * unit isHomotopyInitialNat (I: natOb): U = (C: natOb) * (x: natHom I C) * ((y: natHom I C) -> Path (natHom I C) x y)

Здесь у нас unit-терминейтед record — это что-то типа null-терминейтед стринг. Я думаю идея понятна. Если взять лимит в этой категории получится штука изоморфная черч-кодировке. В HoTT это можно увидеть в параграфе Nat-алгебр (5.4.1) и Nat-гомоморфизмов (5.4.2). Полная кодировка должна включать не только зависимый элиминатор, через который уже выражается рекурсор и кейс анализ, но и правила связывающие фьюжин intro-elim двумя правилами beta и eta которые называются ещё ректракт и секция (enc dec = id, dec enc = id).

Постановка задачи

В этой статье мы покажем, что, во-первых, интернализация MLTT в сущности есть кодировкой изоморфизмами, и, во-вторых, покажем, что в кодировке Пи у нас функция равна своей аппликации (да да, вам не послышалось).

Ну, я думаю не нужно доказывать или показывать, что всё в MLTT есть тип, или всё в мире есть феномен. А раз так, то мы можем построить категорию этих объектов и морфизмов между ними (это у математиков что-то типа если есть гора, то на неё нужно взобраться, или как я называю в любой непонятной ситуации строй категорию). Т.е. тоеретически возможно засунуть любой тип в сигнатуру изоморфизма:

isIso (XML JSON: U): U -- form = (f: XML -> JSON) -- intro * (g: JSON -> XML) -- elim * (s: section XML JSON f g) -- beta * ( retract XML JSON f g) -- eta section (A B:U) (f:A->B) (g:B->A): U = (b:B) -> Path B (f(g(b))) b retract (A B:U) (f:A->B) (g:B->A): U = (a:A) -> Path A (g(f(a))) a

Давайте попробуем это сделать для сложных типов, чтобы доказать первую часть задачи, а потом попробуем закодировать самый базовый Пи-тип на котором строится вся теория MLTT, и докажем вторую часть задания.

Аксиома Унивалентности

Она не золотой грааль, а обычнейший тип, а значит для нее существует 5 правил теории типов Мартина-Лёфа. В сущности, чтобы не лукавить, надо сказать, что унивалентность вшивается в тайпчекеры обычно. В cubicaltt intro-правило типовой унивалентности называется Glue.

univ_Formation (A B: U) : U = equiv A B -> Path U A B -- Formation equivToPath (A B: U) : univ_Formation A B -- Intro pathToEquiv (A B: U) (p: Path U A B) : equiv A B -- Elim eqToEq (A B : U) (p : Path U A B) : Path (Path U A B) (equivToPath A B (pathToEquiv A B p)) p -- Beta idToPath (A B: U) (w: equiv A B) : Path (equiv A B) (pathToEquiv A B (equivToPath A B w)) w -- Eta

Превращаем аксиому унивалентности в енкодер-декодер или изоморфизм:

UnivType (A B: U): isIso (equiv A B) (Path U A B) = (equivToPath A B, pathToEquiv A B,eqToEq A B,idToPath A B)

Неплохо, поехали дальше.

Изоморфизм Изоморфизма

Так как фибрационная эквивалентность есть одним из видов равенства и аксиома унивелентности это в сущности часть конструкции которая связывает фьюжин типов фибрационной эквивалентности Equiv и типа Path встроенного в кубический тайпчекер, то можно построить точно такой же изоморфизм между Path и типом Iso, который так же является одним из видов равенства, простой и поняный всем программистам encode/decode.

iso_Form (A B: U) : U = isIso A B -> Path U A B iso_Intro (A B: U) : iso_Form A B iso_Elim (A B: U) : Path U A B -> isIso A B iso_Comp (A B : U) (p : Path U A B) : Path (Path U A B) (iso_Intro A B (iso_Elim A B p)) p iso_Uniq (A B : U) (p: isIso A B) : Path (isIso A B) (iso_Elim A B (iso_Intro A B p)) p

Заметьте как мы циклически встраиваемся в нижний уровень подсвовывая в сами изоморфизм сигнатуру с изоморфизмом

IsoPathType (A B: U): isIso (isIso A B) (Path U A B) = (iso_Intro A B,iso_Elim A B,iso_Comp A B,iso_Uniq A B)

Пи-тип

Теперь давайте перейдем к самому простому и самому загадночному изоморфизму изоморфизму Пи-типов. Вспомним категорные догматы: чтобы закодировать что-то, нам надо построить категорию эндоморфизмов этого. В нашем случае, так как мы отложили учебник по теоркату и вышиваем на XML <-> JSON сигнатурах, мы просто строим изоморфизм между Пи и Пи:

PiType (A: U) (B: A -> U): isIso (Pi A B) (Pi A B) = (app A B,lam A B,Pi_Beta A B,Pi_Eta A B)
Pi (A: U) (B: A -> U) : U = (x:A) -> B(x) lam (A: U) (B: A -> U) (b: Pi A B) : Pi A B = \(x: A) -> b x app (A: U) (B: A -> U) (f: Pi A B) (a: A) : B a = f a Pi_Beta (A: U) (B: A -> U) (f: Pi A B) : Path (Pi A B) (\(x:A) -> f x) f Pi_Eta (A: U) (B: A -> U) (f: Pi A B) : Path (Pi A B) f (\(x:A) -> f x)

Как видно мы тут немного подхачили, но вполне законно так как мы просто перенесли a : A из телескопа параметров в правую часть результата и протащили в путь: Path (B a) -> Path (Pi A B).

beta_classic (A:U)(B:A->U)(f: Pi A B) (a:A) : Path (B a) ((lambda A B f) a) (f a) Pi_Beta (A:U)(B:A->U)(f: Pi A B) : Path (Pi A B) (\(x:A) -> f x) f

Теперь докажем вторую задачу и главный номер представления (то, что функция равна своей аппликации, ну бредятина же на звук!):

PiType (A: U) (B: A -> U): isIso (Pi A B) (Pi A B) = (lam A B,lam A B,Pi_Beta A B,Pi_Eta A B) = (app A B,lam A B,Pi_Beta A B,Pi_Eta A B) = (app A B,app A B,Pi_Eta A B,Pi_Eta A B)

Любой из этих вариантов чекается!

Checking: PiType File loaded. >

На самом деле, такие тавтологии рождаются потому, что мы в isIso поставили равные типы, до этого в примерах мы делали транспорты из крайних точек пути, тут же у нас петля. Но, тем не менее, этот терм PiType в разных инкарнация вы можете встретить в любой статье про лямбда исчисление, так как он является вычислительной семантикой зависимого лямбда исчисления (для примера классическая запись в виде терма PTS):

PTS (A: U): U = (Pi_Former: (A -> U) -> U) * (Pi_Intro: (B: A -> U) -> Pi A B -> Pi A B) * (Pi_Elim: (B: A -> U) -> Pi A B -> Pi A B) * (Pi_Comp1: (B: A -> U) (a: A) (f: Pi A B) -> Equ (B a) (Pi_Elim B (Pi_Intro B f) a) (f a)) * (Pi_Comp2: (B: A -> U) (a: A) (f: Pi A B) -> Equ (Pi A B) f (\(x:A) -> f x)) * unit

Функциональная экстенсиональность

В качестве бонус трека, funext. В этом примере мы показываем, что терм funext — это все-лишь интро правило, формация же есть классические изоморфизм двух функций f и g, которые находятся в пространстве функций A -> B (в этом примере не зависимых, зависимые вам на домашку).

funext_form (A B: U) (f g: A -> B) : U = Path (A -> B) f g funext (A B: U) (f g: A -> B) (p: (x:A) -> Path B (f x) (g x)) : funext_form A B f g happly (A B: U) (f g: A -> B) (p: funext_form A B f g) (x: A) : Path B (f x) (g x) funext_Beta (A B: U) (f g: A -> B) (p: (x:A) -> Path B (f x) (g x)) : (x:A) -> Path B (f x) (g x) funext_Eta (A B: U) (f g: A -> B) (p: Path (A -> B) f g) : Path (Path (A -> B) f g) (funext A B f g (happly A B f g p)) p

Еще в качестве упражнения функциональную экстенсиональность можно выразить через интервал.

data I = i0 | i1 | seg <i> [(i=0) -> i0, (i=1) -> i1]

В статье только сигнатуры, все пруфы в https://github.com/groupoid/cubical.
Дискас: https://github.com/5ht/tonpa.guru/issues/4




˙