Ладно, вот вам база, почему так трудно переучиваться с императивного/объектного стиля кодинга на функциональный
(утащил у Майкла Шульмана из Univalent Foundations of Mathematics).

В мэйнстриме мы строим типы и данные из простых элементов (int, string, класс, иногда даже sum/product и немножечко lambda/map/reduce). Но это чисто аддитивная сборка: из ничего/примитивов наращиваем структуру, и по сути мышление теорией множеств ("classical set theory is additive synthesis of algebraic structures (start from nothing, add up structure)").

Соответственно, подход абсолютно кривой, чисто инженерный, т.к. эта теория к программированию не имеет никакого прямого отношения :)

Программирование -- это очевидно (далеко не всем:), теория типов прежде всего. И HoTT это по сути тут крайний, "вычитающий" подход (отсекаем от куска мрамра всё лишнее, и получаем прекрасную скульптуру). Стартуем с уже богатой структуры (типы как пространства, равенства как пути, бесконечные слои гомотопий) и получаем нужное, отождествляя, свёртывая, сжимая и отрезая лишнее. Правильное понимание -- это свёртка смысла, это то, что например делает AI при "суммировании"...

Тут мы (как минимум) думаем зависимыми типами, равенствами как структурами, изоморфизмами, путями, это уже чистая логика типов, Карри-Ховард, Coq/Agda/Lean, щедро приправленная (то ли изнутри, то ли снаружи, парадокс:) теорией категорий ("homotopy type theory is negative synthesis (start with categories with infinite layers of homomorphism, carve out structure)").

Именно отсюда и начинается абсолютно правильное, идеальное мышление Программиста. Ну, таким, какое оно и должно быть. В некотором смысле оно ближе к "конструктивной" формальной философии.

"...ибо иго теории категорий благо, и бремя гомотопической теории типов легко есмь" :)