не запрещено так писать в Групоид Инфинити!

разрешено!

но тут концептуально пока не понятно как лучше, будем разбираться в ходе составления либы

мортберг вот всё подряд отрезками доказывает и гордится этим

я согласен с ним

но мы счас в состоянии лишь бы чекнулось )

ну я уже не борюсь с тайпчекером. Но только в рамках примитивов Hott, лямбды вообще не понимаю как работают, хотя вот как делать на лямбдах mapOnPath и inv/sym - научился

ещё кстати побочная программа исследований - запилить https://github.com/alanz/haskell-lsp/blob/master/src/Language/Haskell/LSP/Core.hs#L321

@akuklev нашел темку про Воеводского как было https://mathoverflow.net/questions/234492/what-is-the-mistake-in-the-proof-of-the-homotopy-hypothesis-by-kapranov-and-voev

пейпер про комбинаторный MLTT (ну почти)

@tonpa Поздравляю!

@tonpa поздравляю!)

Спасибо, почитаем сегодня ночью!

Pelayo, Voevodsky, Warren. A preliminary univalent formalization of the p-adic numbers. https://arxiv.org/pdf/1302.1207.pdf

Пока процессор доказывает импредикативную кодировку Эводи в coproduct_set, я решил взять еще одну кодировку, которая описана в работи Эваристы, ученика МакБрайда. Хотя она выглядит как самая программистская (стертая категорная кодировка), она имеет категорные корени в работах Гермиды и Якобса, на который ссылается сам Эвариста.

Таким образом мы в lambek.ctt собираем, все известные описаные модели в пейперах, кодировки индуктивных типов. Их уже несколько:

1. Первая кодировка комутативного квадрата F-алгебры, сигмой из четырех элеметов. [Hinze, Wu] http://www.cs.ox.ac.uk/people/nicolas.wu/publications/Histomorphisms.pdf

2. Кодировка единичными морфизмами Паши Лютко, незаконченная работа, я просто наброски накидал, того, что помню, кто рубит ламбека категорно может продолжить. [Lyutko] http://groupoid.space/mltt/lambek/

3. Кодирвка алгеброй алгебраиков (inductive families) с Агдовским кодом, в котором выражена универсальная индукция для этой модели [Dagand, McBride]. https://pages.lip6.fr/Pierre-Evariste.Dagand/stuffs/thesis-2011-phd/thesis.pdf Попишу ближайшую недельку её.

4. Собственно импредикативная кодировка в HoTT. [Awodey, Speight]. https://homotopytypetheory.org/2017/10/11/impredicative-encodings-of-inductive-types-in-hott/ которой сейчас занимается Андрей в coproduct_set.

5. Кодировка Мотивами для вырежния inductive-inductive определений. Тоже Индуктивные Семейства (индексированне индуктивные типы), в этот раз для моделирования QIT [Altenkirch, Kaposi]. http://www.cs.nott.ac.uk/~psztxa/publ/tt-in-tt.pdf

6. Кодировка Генри Форда или Lan,Kan-кодировка. http://www.cl.cam.ac.uk/~mpf23/papers/Types/gadtif.pdf [Hamana, Fiore].

Та кодировка, в которой проще и быстрее всего выражается индукция, а также та, которая быстрее всего работает, будет кандидатом на основную кодировку теории индуктивных типов в базовой библиотеке. Ну и также свойств, может быть у кодировок сотни, все тут не описать на полях :-)