Я полностью закончил (сделал в смысле :) первый в мире (почему первый в мире? потому что он никому особо не нужен :) курс "Гомотопическая теория типов для программистов (1)", о котором мечтал лет 10-15 назад в духе "эх, вот бы такой когда-нибудь просто закончить (пройти в смысле:)!". Силлабус выложу для курсантов, ну вкратце - интуиционистская версия HoTT, отличия от MLTT, топологическое пространство, гомотопическая эквивалентность, Sum/Product-типы, Path, HIT, n-мерный тор, зависимые Пи-типы и Сигма-типы -- реализуем это всё на Python, все исходники + в тестах разбираем основные use cases, и в заключение делаем на этой базе игру Змейка.

Вторая часть конечно обязательно нужна для полноты (∞-группоиды, гомотопические группы, иерархия универсумов, эквивалентность типов, унивалентность...), но там уже в некотором смысле будет попроще, если проходите, первого HoTT-босса :)

По итогу, всё же должен признать что как я ни пытался задаундгрейдить эти темки до малышового уровня рядового миддла, в целом получилось сложновато. В идеале, реки -- это TaPL Пирса (хотя бы просто понять, без формул). Ну посмотрим.

Самый важный мета-результат, что в процессе я получил правильные инсайты :)

Математика существенно проще, чем программирование.
Это не программисту надо знать математику, а математику надо знать программирование.

Даже самые сильные на сегодня математические абстракции для программистов -- это всё уровень programming in small, максимум programming in large in small. Хотя, безусловно, закрыть теоретически programming in small само по себе неплохой результат.