Почему я у всех этих западных пруверов-шмуверов (далее - Эти) потенциально выигрываю архитектурно? И насколько вообще мои оценки адекватны?

Ну, сегодня к счастью есть достаточно объективные AI-консультанты, шарящие в математике весьма уверенно (вдобавок, напомню, математика существенно проще чем программирование). Я спрашивал и у клода+опуса 4, и у гемини 2.5, и у дипсика и квена с дипсинками, показывал им свой код, и получил очень позитивный фидбэк. Основные претензии чисто у вас недоделано вот тут, а технически не хватает вот этого и того, ну дык, это уже дело времени. Реально очень доволен, даже сам не ожидал 🙏

Потому что всё Это ихнее делалось с нуля, вообще без опыта подобных проектов, а внутри, может их гитхабы посмотреть, это тотальное говнолегаси, которое писали не программисты-архитекторы с многолетним опытом, а преимущественно математики, да ещё и подчас на хаскелях! 🫢

Coq (индуктивные типы и тактики), Isabelle/HOL, Lean основаны на "классических" теориях типов или логике высшего порядка, и вполне обходятся без унивалентности (самая мякотка гомотопической теории). Унивалентность позволяет рассматривать равенство как эквивалентность (изоморфизм) между объектами, что крайне полезно при проверке соответствия интерфейсов или в модел-чекинге.

Я только-только вчера добавил транспорты между путями в ТОП: автоматическое перемещение между "равными" объектами без необходимости явного (ручного) доказательства инвариантов. А у Этих требуется доказывать корректность программ относительно их спецификаций через явные отношения между объектами (изоморфизмы, биекции...), писать крайне громоздкие конструкции для выражения эквивалентности (аксиомы выбора, дополнительные предикаты...). А я потенциально могу работать вообще со "структурами до изоморфизма" (например, в теоркате, при верификации распределённых систем, c гомотопическими типами...).

Кроме того, дальше вообще без проблем добавить "кубики" (чтобы строить модели в конструктивной метатеории, через конструктивную интерпретацию равенства эквивалентных типов), а этот ваш Lean 4 вообще на такое не способен, ну или через кривые приляпки, потому что его реализация использует UIP (Uniqueness of Identity Proofs), что противоречит принципам HoTT, где равенства -- это пути в гомотопическом пространстве (+ кубическая теория позволяет манипулировать "равенствами" напрямую, через операции и композицию 💪🏻 ).