Немного поигрался с лямбда-кубом Барендрегта, пошёл сверху вниз:
CoC я реализовал в 70 строк F#,
затем запилил System Fω (F-омега)
(полиморфизм + конструкторы типов высшего порядка),
затем λP2 (зависимые типы + полиморфизм),
а вот на λPω (зависимые типы + конструкторы типов) сломался.

Просто так полиморфизм из CoC не удалить (Кокан всё же не дурак), надо выстраивать строгую иерархию типов, индексы де Брёйна и всё подобное; по сути надо полностью заменить универсальную архитектуру на иерархическую + жёсткую типизацию.

С другой стороны и хорошо что не вышло, всё равно этот куб на практике не актуален, а CoC и HoTT я реализовал, и куда важнее кубическую теорию дальше (успеть) сделать -- чётко под задачи программиста-миддла. Хотя бы научить рассуждать in small в соответствующих моделях. Например, цепочка конвертации данных с помощью унивалентности (композиция путей соответствует композиции эквивалентностей) с автоматическим доказательством коммутативности преобразований. И постепенно выходим на уровень формального мышления in large.

А без понимания теории типов все проекты будут получаться как на картинке,
но я уже совсем один остался в России в этих темках куда-то ещё едва бреду.....

все уснули давно
в километрах глубин
никого ничего он остался один....

кто сказал что нельзя
переплыть океан
это грустная шутка это хитрый обман...

я сумею доплыть
под сияние звёзд
я хочу увидать край где много берёз...