Interpreting Cubical Type Theory in Appropriate Presheaf Toposes
Jonathan Weinberger

думаю закодировать вот это

U_n is not an n-type: https://arxiv.org/pdf/1311.4002.pdf

Вот еще хороший пример http://www.cse.chalmers.se/~peterd/papers/Catimpl.pdf Cat of Set

Домашка по HoTT: начальный уровень. Доказать, что семейство слоений тотальных отображений эквивалентно зависимой функции.

Больше файбер бандлов! Целый день доказывал простейшую теорему о том, что слоение — это квантор всеобщности, но не сходятся условия ретракта и секции f . g = id_A, g . f = id_B. В беспомощности отправил письмо с просьбой подсказки. Пытался починить фибрации Хопфа, но они не чинятся никак. Инвертирование S1 не дает S1, говорит S1 /= S1 и все. Надо будет попробовать на днях новую ветку hcomptrans. Нарисовал страничку, куда со временем должны попасть фибрации Хопфа. Оказывается то, как я придумал создавать индуктивно сферы называется иерархия суспензий. Сфера S^0 — это булевый тип, две точки. Сфера S^(n+1) — это суспензия сферы S^n, n=0... Cуспензии к счастью в кубике работают. Посмотрел у Спеньера, что для того, чтобы определять всякие разные виды расслоений мне нужна структурная группа.

На выходных читал про расслоения пространств aka Fiber Bundles. FB — это сигнатура F -> E -> B с морфизмами, где F — расслоение (индексированный зависимый тип) [kernel], E — многообразие или топологическое тотальное пространство расслоения, B — база расслоения [image], на которой происходит расслоение. f: E -> B — это проекция или ретракт, s: B -> E — это секция (не всегда существует, так как должно быть f . s = id). Если E = B * F — такое расслоение называется тривиальным. Так вот если F взять Pi или Sigma вы получите сопряжения кванторов. Если взять вместо F — R^n вы получите расслоение векторных пространств. Факторпространства и расслоение сфер — другие примеры расслоений. Лента Мебиуса — это расслоение линии сегмента по окружности, секция такого расслоения перекручена. Бутылка Клейна — это расслоение окружности по окружности, когда сецкия такого расслоение перекручена. Пока писал пост, успел купить книгу и сформулировать определения на кубике.

TL;DR Импредикативные кодировки индуктивных типов в HoTT

Все, кто хоть раз писал по настоящему на LISP знакомы с кодировкой Черча, в CoC она тоже есть завтиповая, мощная (Morte, Om — языки СoC). В ней NAT = (X:U) -> (X -> X) -> X -> X, где первый аргумент (X -> X) — это succ, а второй X — zero, и результат — во вселенной кодируемого типа Х. Даже если мы закодируем тип с параметром LIST (A: U) = (X:U) -> X -> (A -> X) -> X, и параметр A будет во вселенной 42, а X во вселенной 2, то кодировка всегда будет лендить терм в Х, т.е. во вторую вселенную, в не зависимости от A. Такая зависимость термов называется импредикативной и не работает, например в предикативной или предикативно-кумулятивной иерархии вселенных.

В HoTT номера n-types кодируются n-групоидами, поэтому в кодировку нужно добавить предикат в каком n-типе лендить терм Х: NAT  = (X: U) -> isSet X -> (X -> X) -> X -> X, тут появился предикат isSet. С его помощью можно реализовать пропозишинал транкешины ||-|| (лендинг в Prop) и даже HIT (лендинг в Groupoid, например, для окружности):

1) Truncation ||A|| parametrized by (A:U) type = (X: U) -> isProp X -> (A -> X) -> X
2) S^1 = (X:U) -> isGroupoid X -> ((x:X) -> Path X x x) -> X
3) Arbitrary (A:U) type = (X: U) -> isSet X -> (A -> X) -> X

На картике приведена кодировка Unit (кроме eta), которую написал Мельников, а я лишь слегонца упростил и убрал лишнее. Кодировка обычного Nat тянет на магистерский проект. Общая схема — PhD и открытый вопрос в теории типов.

TL;DR Конструктивное доказательство унивалентности

Пресловутый терм унивалентности, доказанный с помощью кубических примитивов Glue — склейка типов, glue — склейка значений, fill — пополнение Кана (типа дорисовать ребро квадрата), comp — склейка двух путей (дорисовка ребра треугольника), <i> — следует читать как лямбда определенная на орезке [0,1], \ — обычная лямбда, * — сигма. Это и есть почти-нормальная форма (idEquiv только заэкспандить), которая тоже помещается на экран.

Море новостей. Во-первых чтобы конструтивно бандлы смоделировать и что-то "посчитать", то посчитать можно только Структурные группы aka Covering Spaces и G-structures, на смоделированых через фломальные étale мапы многообразиях. Так можно смоделировать векторные бандлы и посчитать ихние группы автоморфизмов. Бывает так, что и сам слой F является группой афтоморфизмов. Так вот étale мапы моделируется через интересную штуку — модалити, она есть в конце первой части HoTT, но не испольузется дальше в книге нигде. Бандлы — это вообще самая главная часть алг. топологии, есть в каждом учебнике, можно сравнить определения, но самое интересное — это PhD Феликса Веллена http://www.math.kit.edu/iag3/~wellen/media/diss.pdf где формализируется на Агде то, про что я сейчас рассказал. Чтобы вы не рылысь в его исходниках я выдер только эти определения, еще там есть 4 равнозначных определения расслоеных пространств, определение модальностей, étale морфизмов на них, многообразий на этале морфизмах, определение G-структуры на Автоморфизмах и фундаментальный инфинити групоид в виде индуктивного типа Майкла Шульмана. Вес это я занимает 500 строчек на Агде https://github.com/groupoid/infinity/blob/master/priv/bundle.agda. Нашел еще классные слайды Favonia (к которому обращается Роберт Харпер в своих лекциях 15-819) https://www.math.ias.edu/~favonia/files/cover-crm2013-slides.pdf которые показывают, что G-структыры эквивалентны Накрывающим Пространствам.