Есть такой умник, французский математик Thierry Coquand, один из главных авторов легендарного теорем-прувера Coq (Thierry и назвал его так по своей фамилии), который теперь Rocq -- ключевой инструмент в европейских университетах по обучению всяческим формальным темкам, и куда нам теперь путь навсегда заказан.

В основу своего петушка Кокан заложил собственную теорию типов Calculus of Constructions (CoC): типизированное λ-исчисление + логика высшего порядка + полиморфизм, через изоморфизм Карри-Ховарда.
И это конечно топчик λ-куба Барендрегта, да, но...

В CoC эквивалентность типов (изоморфизм) не означает их равенство. А вот гомотопическая теория типов Воеводского HoTT вводит аксиому унивалентности, которая отождествляет эквивалентные типы.

В CoC равенство определяется через лейбницевский принцип неразличимости тождественного. В HoTT он заменяется на тип путей Path (непрерывная деформация), а доказательства равенства становятся конструктивными (например, гомотопии), что позволяет естественно кодировать высшие категории или ∞-группоиды например. При этом сохраняется canonicity: программы на основе HoTT можно выполнять, а доказательства верифицируются алгоритмически.

хотт - это язык программирования Бога

Владимир Воеводский реализовал свои гениальные идеи HoTT в библиотеке Coq через расширение CIC (Calculus of Inductive Constructions). Он по сути трансформировал применение Coq, показав, что формальные системы могут кодировать не только логику, но и глубокие геометрические структуры.

Но в итоге два ведущих теорем-прувера + языка с заптипчиками - Coq/Rocq и Lean - решили развиваться в направлении усиления CIC, и по сути отказались от HoTT в своих движках, во многом из-за их архитектурной кривизны. По большому счёту это стратегическая ошибка, пояснял тут.
И это прям очень-очень радует 💥💥💥