>>448
型理論。

MLTT 型理論にUnivalence Axiom を足したもん。

何が嬉しいかって、プログラミング言語なの。この理論。