...Более того, понимание теории типов позволяет нам заявить, что не только F# и Java -- совершенно разные языки, что в принципе достаточно понятно со стороны (F# -- это всё же функциональный язык с алгебраическими типами), но и
C# и Java сегодня -- совершенно разные языки.
Мейнстрим тут способен мыслить лишь на школьном уровне "статическая типизация", "ООП-парадигма" ...

Java строго номинативен: все пользовательские типы (классы) сравниваются по ссылкам, даже если поля идентичны, а проверка структурного равенства (когда эквивалентность типов определяется их поведением, а не именем: формальная версия утиной типизации) требует явного переопределения equals().
В C# же не только есть сишные структуры (для которых структурное равенство работает по определению:), но и с 9й версии - records (автоматическая реализация структурного равенства).

Делегаты C# (Func<T>, Action) — это структурно-совместимые типы функций. Два делегата с одинаковой сигнатурой считаются совместимыми, даже если объявлены по-разному.

В Java же наоборот: функциональные интерфейсы (Runnable, Consumer<T>) номинативно зависимы: даже если сигнатуры методов совпадают, интерфейсы несовместимы без явного наследования.

С точки зрения HoTT это критично: в C# функции могут быть "путями" между типами, без явных преобразований, а в Java требуется явное приведение через адаптеры (например, лямбды - к разным интерфейсам). А если же мы хотим в C# неявные преобразования, есть классный implicit operator.

В C# информация о типах при использовании генериков сохраняется в рантайме, что позволяет проверять структурные преобразования динамически. В Java же генерики реализованы через type erasure (на что я уже напоролся в Python при реализации HoTT :), что делает их номинативными и невидимыми во время выполнения.

Гомотопическая теория ближе к идее "типы как объекты", когда преобразования типов можно анализировать на втором логическом уровне.

Короче говоря, в терминах HoTT,
Java навязывает жёсткую иерархию именованных типов,
а C# позволяет работать с типами как пространствами, где изоморфизмы (эквивалентности) могут быть частью самой системы типов!