Я закончил таки кубическую теорию (всего за 200 долларов на клода4), было очень тяжело, местами несколько раз даже думал что вообще не справлюсь. Засада в том что подтянуть готовую реализацию из HoTT не получается, кубики это по сути самостоятельная теория типов, и в итоге пришлось делать её полностью с нуля. Но с другой стороны это и хорошо.

Базовые структуры для работы с кубами (Interval, Direction, Face, Cube, System); механизмы для работы с путями и транспортом типов; реализация эквивалентностей и унивалентности, базовые Higher Inductive Types.

Кубические пути позволяют формально описывать и проверять трансформации между типами данных. Транспорт типов (CubicalTransport) обеспечивает безопасную миграцию данных при изменении структуры типов. Эквивалентности (CubicalEquivalence) гарантируют сохранение свойств при рефакторинге.

N-мерные кубы (Cube) естественно моделируют пространство состояний параллельных процессов. Система правил (System) позволяет описывать допустимые переходы между состояниями. Композиция Кана (Kan composition) обеспечивает корректное слияние параллельных изменений.

Higher Inductive Types позволяют определять абстрактные типы данных с встроенными инвариантами. Пути (CubicalPath) формализуют допустимые преобразования данных.

Унивалентность (Univalence) обеспечивает перенос свойств между эквивалентными представлениями -- она становится вычислимым свойством (реализуется transport типов), а не просто аксиомой, как в HoTT, что делает CTT более практичной.

И теперь у меня полный комплект: HoTT, CoC, CTT.