Ожидание:
HoTT в Lean 4: 3/10 (почти готовая реализация)
HoTT в Python: 10/10

Реальность:
HoTT в Lean 4: 8/10
HoTT в Python: 5/10

Вот этот контринтуитивный момент стал для меня пожалуй самым важным пониманием - из реальной практики - и на него не жалко было потратить несколько сотен долларов. В принципе я как-то интуитивно предполагал:
"...4. MLTT++ на Python по-взрослому (термы/значения как типы данных)."

Поэтому взялся сперва за Lean4, в иллюзии что уж на его крутой системе типов запилить гомотопическую теорию вообще легко и просто, но ведь я сам и писал:
"...Это как попытка встроить квантовую механику в классическую физику: принципиально новый уровень абстракции."

Ровно так и получилось: оказывается что чем сильнее система типов, тем будет не легче а тяжелее реализовывать на ней сложные абстрактные темки. Многие годы до вчерашнего дня я считал 💯 что чем она сильнее, тем в любом случае будет проще и быстрее , при надлежащем уровне понимания, что угодно на ней реализовывать -- но нет.

Теперь совершенно не исключаю что вот именно уровень C# или Python с аннотациями типов и есть как раз тот самый оптимальный баланс относительно реальных прикладных практических задачек которые можно реализовывать с какой-то формальной поддержкой со стороны HoTT.
Буду над этим отдельно много думать, и что с этим пониманием делать дальше.

Конечно моя реализация в некотором смысле игрушечная: type inference "на уровне компиляции" в ней отсутствует по сути более чем полностью, и насколько она потянет конструкции на сотни, а тем более тысячи, термов, вопрос пока открытый. Хотя конечно чисто технически, уверен, это вполне можно будет решить.
Пока всё уместилось в тысячу строк кода, и думаю что теперь уже не будет особых проблем автоматически конвертировать его на PHP или C++. Отдельно хочу попробовать "обратную" схему: из Python-реализации в Lean :)

Ну и буду дальше изучать/экспериментировать с тем что получилось. Ещё вчера я приунывал, что не получится прыгнуть выше MLTT, а сегодня уже думаю, как бы сделать киллер вообще всех систем топового уровня, наподобие lean, f*, agda, coq )))

Потому что у меня всё же цель не продакшен, а обучение этому всему.