...В принципе можно конечно сделать вообще на Лине 4, самое смешное, что поддержка хотт была в третьей версии, но потом её оттуда выпилили, потому что поддержка унивалентности в ядре Lean оказалась пацанам не под силу 😬 Надо переопределять базовые понятия равенства, конфликты с классическими представлениями о тождестве, нарушается UIP и AC, бесконечные иерархии преобразований, запутанные проверки эквивалентности...

Вроде бы тривиально?

def idEquiv {A : Type} : A ≃ A

Да но мы-то хотим такое с унивалентностью в ядре доказательств 🫢
Классическая теория, что с лицом?

Это как попытка встроить квантовую механику в классическую физику: принципиально новый уровень абстракции.

Поэтому с одного края: то что я делал на PHP, просто закодировать непосредственно на лине как языке программирования (без каких-то плагинов для ядра), это вообще легко и просто. Но тут засада, что я ведь хочу сделать многопользовательский (веб)клиент. Хотя в лине имеется нативная поддержка concurrency, асинки...

1.1. Посмотреть, можно ли на коленке склепать рестик на лине 4.
1.2. Запилить некую минималистичную поддержку хотт.

=

Другой вариант: использовать F* -- микрософт его прям энергично развивает вовсю. И вроде бы это .NET -- но нет )
Сетевой поддержки у него нету, придётся делать обвязки на ocaml, да и сам он позиционируется прежде всего в направлении верификации кода, Lean конечно посильнее в математическом плане.

Поэтому от F* отказываемся, и следующий шаг -- это наш любимый F#. Вот тут в техническом плане сразу всё становится элементарно, но зато мы резко проседаем по системе типов (прежде всего теряем завтипчики) и уже прилично скатываемся на другой конец, ближе к пыхапы 🙈

Навскидку:
HoTT в F#: 7/10 (практически с нуля)
HoTT в Lean 4: 3/10 (почти готовая реализация)

2.1. Если по п.1.1 возникнут явные трудности, когда немного поэкспериментировать с F#.

(размышления продолжаю...)