Cartesian Cubical Type Theory

Все вы знаете уже, что с августа 2017 года конструктивную интерпретация аксиомы унивалентности можно доказать не только на бумаге, но и используя тайпчекер cubicaltt. Но мало кто знает, что этот тайпчекер является устаревшим! Да да, начиная с марта 2018 года появилась новая конструктивная кубическая теория и ее тайпчекер yacctt, основанная не на примитивах композишина и склеек comp Glue glue, а на коершинах и гомогенных композициях coe, hcom, box, cap, а вместо glue — V-типы (в yacct две иерархии вселенных: претипы и типы Кана). Хотя и то и другое — операции Кана, последняя модель позволяет получить более компактные доказательства и более компактный тайпчекер. Основная мотивация такого пайвота в том, что на кубике не считается число Брунери n=2 в π_4(S^3) ≃ Z/nZ (канонический тест для гомотопического тайпчекера). Для этого оказывается 64ГБ памяти маловато! Правда на yacctt еще пока не написано, но уже видно, что основные унивалентные теоремы гораздо компактнее.

Всего существует 5 флейворов кубической теории:

1. cubicaltt: \(i: I)->, i @ x, сomp, /\, \/, ~, Glue, glue, unglue;
2. yacctt: \(i: I)->, i @ x, hcom, coe, V, Vin, Vproj;;
3. Arend, redtt, RedPRL: \(i: I)->, i @ x, coe, V, Vin, Vproj;;
4. hcomptrans: \(i: I)->, i @ 0, /\, \/, ~, hcomp, Glue, glue, unglue;
5. Agda: \(i: I)->, i @ x, hcomp, comp, \/, /\, ~, coe, Glue, glue, unglue

Как видно больше всего пруверов написано именно под эту Харперовскую версию кубической теории. В том числе и новый прувер Arend от JetBrains, про который я обязательно напишу обзор потом.

Также эта теория типов находится внутри тайпчекера RedPRL с вырвиглазным NuPRL-овским синтаксисом для любителей говна мамонта, таких как я! Но у нас в базовой либе гораздо больше термов, RedPRL по сути голый, без термов. Но! У меня появился новый способный ученик, который возможно будет портировать нашу базовую библиотеку на RedPRL, по крайней мере я полностью обещал помогать ему в этом. Мортберг также контрибютор RedPRL, написанный на божественном MLton. Основные контрибуторы Favonia (главный ученик Харпера), Карло Анджиули (соавтор yacctt с Мортбергом).

[1]. Презентация Мортберга
[2]. Тайпчекер
[3]. http://www.redprl.org/en/latest/
[4]. Статья: https://arxiv.org/pdf/1712.01800.pdf