1. Параметрический полиморфизм -- это база универсальности.

2. ad-hoc полиморфизм -- это зависимые типы.

3. Сабтайпинг ("наследование") -- это эквивалентность.

Circle -- подтип Shape. Везде, где ожидается Shape, можно использовать Circle.
Профит! )))

(На самом деле, тут немеряное количество засад даже на уровне базы SOLID, особенно по LSP; всё это подробно, с анализом в ФП, разбирал в большом гайде)

По-взрослому же, в HoTT используется эквивалентность типов и унивалентность. Если тип Circle можно преобразовать в тип Shape, то это преобразование считается "путём" между типами. А унивалентность гарантирует, что если такой путь существует, то он по сути и есть "правильное" "наследование". Другими словами, любое свойство, доказанное для всех Shape, автоматически выполняется и для Circle (потому что с точки зрения логики предикатов они находятся в отношении эквивалентности).

Классическое наследование -- это частный случай построения такого "пути-функции" из подтипа в супертип.

При этом мы получаем все "инженерные" фишки ООП (SOLID и Co) "в коробке", за нас всё делает HoTT-"движок". Например, в Shape есть area() (вычисление площади), которая всегда должна быть положительной. Но в реализации Circle она может быть нулевой, и тем самым мы нарушаем LSP.

В HoTT же "нарушить LSP" технически невозможно: система типов (топовая в мире на сегодня) гарантирует, что все случаи обработаны корректно. Подтипизация тут моделируется через эквивалентность, которая сохраняет все свойства: если какой-то подтип не удовлетворяет всем свойствам супертипа, то мы просто не сможем доказать эти свойства для супертипа, и значит, не сможем применить их к подтипу.

Другими словами, при нарушении LSP (и многих других солид-шмолид etc) мы получим ошибку компиляции.

=

Другое дело, что сегодня таких "языков программирования", реализующих HoTT (или хотя бы просто завтипы), которые можно было бы считать массовыми хотя бы на 2%, нету и особо не ожидается (в первую очередь потому, что умненьких очень мало, а будет ещё меньше:).

Но, конечно, в проектах формальной верификации (крайне дорогих) только они и применяются (Coq, Lean, Agda...). Полагаю, что в итоге всё программирование к этому и сведётся: будет либо дерьмовый и дешёвый вайб-кодинг со школотой, либо дорогое качество (верификация AI-кода) с элитой. И никакого промежуточного слоя, и никакой возможности лифтинга на топовые уровни.

Думайте.