Первые ошибки на слайдах пофиксал и выложил как отдельный репо на гитхабе, шлите ваши пулл реквесты, ишьюсы и звезды https://github.com/groupoid/cafe, Там же появится ссылка на видео. Считайте это итоговым отчетом о проделанной работе за 2 года учебы.

Добавил пример из HoTT учебника для Real (Junior) Hopf Fibration. Оказывается расслоение там — это Мебиус стрип, только не отрезок крутящийся умноженный на окружность, а bool умноженный на окружность (нетривиальное равенство S1 заменяется на нетривиальное равенство bool, где bool — это сфера размерности ноль!). Начал искать, где написано, что Real Hopf Fibration является Мебиусом, но кроме ncatlab упоминания про это нигде нет. Кто знает — поделитесь приватно! Осталось доказать равенство прямых произведений расслоений на свои базы своим тотальным пространствам (для Complex Hopf Fibration испольузется факт того, что Join S1 S1 = S3, для Junior — попроще, так как край Мебиуса тоже окружность — можете сразу брать в качестве домашки!).

Технический момент: поскольку HIT (единственные работащие в мире) есть только пока в ветке hcomptrans, я Хопфа сложил в папке hcomp в репозитории инфинити. Эта же папка будет включать порт нашей базовой библиотеки на ядро hcomptrans (тоже кстати можете начинать сами резать на файлы и ознакамливаться с кодобазой, пул реквесты обещаю принять!). Для профессоров и докторов (если такие есть на канале, а такие есть!) рекомендую сразу переходить к Quaternionic Hopf Fibration, по индукции, там она есть, просто она гипернетривиальная :-) Octanionic Hopf Fibration с вашего позволения оставлю себе, но если вы закомитите — обещаю не сопротивляться!

Еще один файндинг: в процессе детального разбирательства с комплексным Хопфом, "обнаружился" изоморфизм Helix (бесконечной пружины) и Гомотопических Действительных Чисел. Этот изоморфизм тянет на домашку, поэтому делюсь с вами:

Helix:

sucPathZ : Path U Z Z = isoPath Z Z sucZ predZ sucpredZ predsucZ
helix : S1 -> U = split { base -> Z ; loop @ i -> sucPathZ @ i }

Homotopical Reals:

data R = cz (x: Z) | sz (z: Z) <i> [(i=0) -> cz z, (i=1) -> cz (sucZ z)]

Красивый пример! Напоминаю, что все это есть в учебнике HoTT и я ничего не придумываю! Очень нравится, что в учебнике HoTT в качестве домашек приведены открытые проблемы теории типов! Еще больше нравится то, что половина из них закрыта кубиками :-)

Про гомотопические группы сфер. Число Брунери (двойка) из  π₄(𝕊³) ≃ ℤ/2ℤ пока не считается ни в одном кубике (включая hcomptrans), вылетает по памяти на машине с 64ГБ ОЗУ, у меня на домашней всего 32ГБ, так что нужно занятся этим вопросом серьезно. Подумывают даже о пост-кубических теориях, расширив ядро новыми примитивами, которые могли бы помочь этому вычислению, но пока неясно какие это могут быть примитивы. Моя мысль сводится к тому, чтобы зарефакторить πᵤ(𝕊ⁿ), piS:

module euler where
import trunc
import pointed
import suspension

piS (u: nat): nat -> U = split
  zero   -> sTrunc (space (omega u (bool,false)))
  succ x -> sTrunc (space (omega u (Sn (succ x),north)))

потом найти машину с 256ГБ ОЗУ и попробовать закрыть первыми конструктивный вопрос о четвертой гомотопической группе трехмерной сферы, но что делать дальше понятно не очень и не многим. Если получится — будем первыми, кто увидел в консоли терминала число Брунери — succ (succ zero)!

у меня есть)

Университетский HPC?

да, но по факту в личном пользовании почти

Так, это некислая мотивация, придется ускориться с портированием!

а сколько по времени надо?

Ну это ж искусство, как пойдёт, кроме того там сложная математика, и Хопф задействован. Буду держать в курсе продвижения. Так то, работы на месяцы. Придётся остановить все активности и заняться только этим!

ну я имел ввиду сколько процессорного времени примерно надо

64ГБ заполнились за 8 часов вроде, но то дохлая машина. Если это HPC должно быть веселее, возьму в соавторы! Неплохо было бы тайпчекер на Rust переписать, но это слишком большой пайвот.

👍

Так, похоже я погорячился!
"Right now Favonia is running the computation with a machine with 1TB of RAM, and it’s been running for … 90 hours or something, and we don’t know yet what will happen."
https://thehighergeometer.wordpress.com/2018/06/29/trying-to-compute-bruneries-number/
:-)

охх

-- Shape Modality (Fundamental $\infty$-groupoid)
data shape (A: U)
     = sig' (_: A)
      | kap (_: R -> shape A)
      | kap' (_: R -> shape A)
      | p1 (g: R -> shape A) (x:R) <i> [(i=0) -> g x, (i=1) -> kap g]
      | p2 (x: shape A) <i> [(i=0) -> x, (i=1) -> kap' (\(_:R) -> x)]

data R
     = cz (x: Z)
      | sz (z: Z) <i> [(i=0) -> cz z, (i=1) -> cz (sucZ z)]