Классический университетский подход к обучению гомотопической теории типов, судя по всему берёт своё начало с 2012-го года, когда в Институте перспективных исследований IAS целый год был посвящен темке "унивалентных оснований математики", который объединил исследователей из разных математических традиций, а результатом стала знаменитая "HoTT Book".

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

Например профессор Андрей Бауэр из Люблянского университета, один из ключевых авторов книги, разработал докторский курс, который намеренно сочетает абстрактные и конкретные элементы, подразумевая, что студентам сначала надо развить интуицию в классической теории, и только затем перейти к синтетическому представлению.
Ну наверное, если там готовят именно математиков... Сперва им например для разминки предлагается поразбираться в локально тривиальных расслоениях и модельных категориях Квиллена :)

В университете Карнеги-Меллона проводился исследовательский семинар по HoTT, где сперва изучали конкретные пространства (окружность, интервал, сфера, тор), а затем перешли к абстрактным понятиям (унивалентность, транспорт вдоль путей)...

=

У нас ничего подобного не будет, минималистичную базу HoTT по моему курсу программист-миддл сможет изучить с нуля за один час (надеюсь...). Что интересно, когда я только начал прикидывать код для высших индуктивных типов Окружность и Тор, буквально на автомате зафигачил класс, который их обобщает до произвольного количества дырок в пространстве, а сами эти классы получаются просто частные случаи-наследники. Ну просто потому что не имеет смысл сперва писать отдельно класс Окружность (одномерное пространство), затем отдельно Тор, где надо "удвоить" код Окружности, и т.д.

Я же это чисто по-программистски сделал, ну и в целом, как учит функциональное программирование, всегда лучше использовать генерики вместо конкретных типов: абстрактный подход позволяет сразу увидеть общие структурные свойства, не отвлекаясь на детали конкретных примеров. Но так почему-то в математическом мейнстриме не учат.

А вот отче наш Гротендик (на фото) в работе "Sur quelques points d'algèbre homologique" использовал категории сразу для определения и построения более общих теорий, которые затем применял к конкретным областям, включая алгебраическую геометрию.

То есть хочу сказать, что развитое программистское мышление даже самые продвинутые теории типов должно понимать достаточно легко и просто, причём уметь задействовать их значительно лучше в прикладном смысле, нежели математики.

Сегодня эти темки особо актуальны: когда я разбирался с реализацией Тора, заинтересовался, что оказывается этот тип эквивалентен произведению двух окружностей, о чём есть соответствующий материал некоей Кристины Соджаковой.
Эта женщина мощный математик, работает конечно же on the formal verification of cryptographic protocols (а также над криптой:), и HoTT в этом одно из ключевых направлений. Правда действующих специалистов в этом в мире вряд ли наберётся хотя бы 5-10 человек.

Вот и хочу поставить такой эксперимент: если обучить этим темкам достаточно большое множество сильных программистов (и только в России), что будет в результате?