Дружественный к Групоид Инфинити канал, начавший транслировать основы современной алгебраической топологии, встречаются даже примеры на кубике: https://t.me/systemflow рекомендую! Говорят авторство принадлежит https://awkure.github.io/ У меня тоже есть одна переведенная статья на русском про Хроматическую Тегорию Гомотопий, авторства Jonathan Beardsley (дайжест книги  "Нильпотентность и периодичность в стабильной теории гомотопии" Дугласа Равенела), которую возможно стоило бы выложить на Групоиде или выложить на этом канале в качестве гостевого поста :-)

|￣￣￣￣￣￣￣￣￣￣￣￣￣|
|  quasicategories are just       |
|  one kind of (∞,1)-category  |
|  there are many other kinds  |
|  please be more precise        |
|＿＿＿＿＿＿＿＿＿＿＿＿＿|
            (\__/)   ||
            (•ㅅ•)  ||
           /  　  づ

Порезал для вас HoTT на А5 двухтомник. Программирование и Математика отдельно. Заказ в любую точку планеты Земля. Издатель Проект Баловство. Цена за два тома составляет $35. Ни я ни издатель не получаем ни копейки (просто себестоимость печати).

2:00 AM Заказал три комплекта, два из которых у меня уже забрали, оставил один себе, так что у меня уже ничего нет, заказывайте на сайте!

https://balovstvo.me/hott

круто! дякую

Також на лекції буде розіграш цих двох книжок! Та, що зліва — за саме глибоке та фундаментальне питання. Та, що справа — за максимальну кількість репортаж-постів у соцмережах (наприклад). Хаха. Вона просто дорога і товста, і я по ній Coq вчив (і навіть дещо написав), так що за неї доведеться поборотися. А ліва книжка — це та з якої все почалося — стаття Пера Мартін-Льофа за 1972 рік (спряжені квантори, логіка, канонічність нормалізації). Перша стаття по теорії типів, яка є фундаментом HoTT (Перша глава). Були ще версії за 1975 (предикативність, всесвіти) та 1984 (тотожність, терміновані дерева, натуральні числа, списки, скінченні множини). Сподіваємося, що видавництво "Баловство" підготвує також версії за 1975 та 1984 роки, або видасть усі три однією книгою!

Пацаны, из Москвы к нам приехал @n_poch (едет в Киев из Ирпеня), и мы с ним решили спотнанно провести внеочередное заседание подольского коммитета HoTT приуроченное к лекции 25-го числа. Еще один член коммитета @Karkunow тоже подтянется после 20:00. И вы, @darkproger, Kostiantyn подтягивайтесь! А где Немиш, почему его нет в группе? — я слышал он протестует против Телеграма.

Norm posideli!

Поразительно, инфинитиземальный тип, который я портировал для этальных морфизмов подходит оказывается и для формализации теории узлов в HoTT. Как сообщает Урс Шрайбер в рассылке HoTT на гуглогруппах, сооснователь ncatlab и один из разработчиков Cohesive Топосов, также топ-специалист по инфинити категориям.

57 слайдов получилось, is this prime number?

Сегодня целый что называется рисерчил. Но перед репортом за сегодя — предистория. На прошлом заседании подольского коммитета HoTT было принято решение занятся в топовом варианте как ближайшие глобальные задачи формализацией CW-комплексов и тегории Гомологий (и для того и для другого есть формализация в HoTT-Agda и мы на нее активно смотрим).

Естественным образом метатеория HIT является тегория цепных комплексов, так как Iso(CW-complex,HIT). Поэтому любая либа CW-комплексов неплохо, чтобы была одновременно и метаторией для HIT и удобным инструментов в руках математика, в том смысле, чтобы хорошо ложилась хотя бы на аглоязычных авторов по кусочно-линейной топологии (Рурк, Сандерсон). В идеале, конечно, построение категории CW-комплексов (их интернализированых моделей) вместе с морфизмами.

Как известно из последнего пейпера https://arxiv.org/pdf/1802.01170.pdf, самый современный HIT вычислитель построенный в 2018 — это hcomptrans ветка кубика, где поддерживаются рекурсивные HIT, Hopf, Trunc и другое. Структура гомогенной композиции, прямо прописывается в начальную алгебру индуктивного типа HIT внутри кубического тайпчекера. Вот пример доказательства, что гомогенная структура единичного квадрата равна 2-сфере заданной с помощью одной точки.

data sph = pt | surf <i j> [ (i=0) -> pt, (i=1) -> pt, (j=0) -> pt, (j=1) -> pt ]

Square (A : U) (a0 a1 b0 b1 : A) (u : Path A a0 a1) (v : Path A b0 b1)
 (r0 : Path A a0 b0) (r1 : Path A a1 b1) : U
 = PathP (<i> (PathP (<j> A) (u @ i) (v @ i))) r0 r1

sqSurf (x: sph): Square sph x x x x (<i> x) (<i> x) (<i> x) (<i> x)
 = <i j> hcomp sph x [(i=0) -> <i> x, (i=1) -> <i> x, (j=0) -> <i> x, (j=1) -> <i> x ]

loop2   : Path (Path sph pt pt) (<i>pt) (<i>pt) = sqSurf pt
loopSph : Path (Path sph pt pt) (<i>pt) (<i>pt) = <i j> surf {sph} @ i @ j

loopEq : Path (Path (Path sph pt pt) (<i>pt) (<i>pt)) loop2 loopSph = ? — упражнение для моих учеников

Таким образом стал вопрос, а что, если мы для построении базовой библиотки CW комплексов встроим ее модель в кубический тайпчекер (интернализируем, как мы проделали с Теорией Типов в mltt.ctt). Что мы хотим от модели CW-комплекс, или скорее, что хочу я от нее. Я хочу, чтобы можно было делать кейс-анализ по отдельным n-ячейкам CW-комплекса, а не трактовать экземпляр индуктивного типа как шейп, хочу иметь возможность выбирать точки и открытые отрезки, открытые плоскости, открытые окресности и с помощью кейс-анализа производить декомпозицию комплекса. В то же время хочу иметь возможность трактовать CW-комплекс как коиндуктивный тип, который полностью заполнен экземплярами своих конструкторов (сигма тип или рекорд).

Кстати вы не можете написать функцию S^1 -> bool, так как нарушается связность шейпов и кубик не разрешает скажем сплитнуть base в false, а loop в true, и ни один кубический тайпчекер, что создает немалые преграды для библиотеки CW-комплексов и ее интернализированной версии.

data bool = false | true
data I = N | S | M <i> [(i=0)->N,(i=1)->S]
isOpen: I -> bool = split
 N -> false
 S -> false
 M @ i -> true — this includes edge cases N and S !!! split HIT for proving not for runtime, be careful

> ERROR

Главная проблема в HIT, как объяснил Мортберг — это фикпойнт в рекурсии (конечно же) и фибрационная семантика параметров в зависимых типах, которую надо включать в гомогенную структуру композиции. Если без параметров, то все просто, а с параметрами завтиповой теории — по сути паралельный лямбда вычислитель (Воеводский гомотопическую теорию называл HTS системой с двумя лямбдами: путь и пи),телескопы за собой завтиповые тягать, вообщем хочешь HIT построить будт добр еще два раза завтиповую лямбду прикрутить и ее контексты, категории контекстов CwF, выше уже нет смысла формализировать лямбда вычислители (на мой взгляд). Конечно это все очень сильно с уклоном в компьютер сайнс а не настоящую рабочую библиотеку CW-комплексов работающего математика.

Основная идея здесь, что мы строим свой телескоп в котором должны держать все n-клетки в одном списке (структура усложнится, здесь список просто чтобы показать идею), идеально было бы что были ссылки на клетки предыдущих размерностей в структуре с помощью завтиповой параметризации, и генерация AST кубика по модели, в идеале с нагенерированными рекурсорами! Это выходные я провел с веткой hcomptrans.

IS THIS A BALL ?

data ball (x: sph) = bo (x: sph) | space <i j k>
[ (i=0) -> bo x, (i=1) -> bo x ,    
  (j=0) -> bo x, (j=1) -> bo x ,
  (k=0) -> bo x, (k=1) -> bo x ]

http://groupoid.space/mltt/types/cw/