...И вернулся наконец к "Гомотопической теории типов для программистов".
Некоторые определения пока получаются рекурсивными )))

Например когда изучаем абстракции Петель и Путей, приходится добавлять понятие Базовой точки. Так-то все эти понятия по большому счёту на уровне алгебры и геометрии обычной старшей школы. Например, петля — это путь от точки к самой себе :) И третьеклассник поймёт.

Базовая точка здесь принципиально важна, так как именно относительно неё формируется петля, но засада в том, что от базовой точки измеряются все гомотопические эквивалентности, которым соответственно надо дать отдельное определение. Тут мы добираемся до pointed типа, который позволяет определить конструкции, зависящие от конкретной точки отсчёта (например, фундаментальная группа пространства). Теперь надо разобраться с первой гомотопической группой, и с рекурсивными определениями функций из высших индуктивных типов в другие типы, однако до HIT мы ещё не добрались, а когда берём высший индуктивный тип Окружность, смотрим, почему фундаментальная группа окружности изоморфна группе целых чисел Z, откуда возвращаемся к гомотопической эквивалентности и группе петель...

Но что интересно, все эти рекурсивные определения весьма неплохо понимаются 🙃
Просто терминология такая математическая, но на самом деле сами понятия весьма простые, делаем их наглядные реализации на Python.

Попутно откопал классный разбор на пальцах этих темок в нескольких абзацах с картинками. Так-то это второй третий курсы универа, или даже физ-мат школы.