Univalence Axiom

The univalence axiom is the cornerstone of homotopy type theory, proposed by Vladimir Voevodsky. It asserts that equivalent types are equal — formally, that the map from equalities to equivalences is itself an equivalence.

In practical terms: if two mathematical structures are isomorphic, then univalence treats them as identical for all purposes. This collapses the distinction between 'the same structure expressed differently' and 'the same structure,' eliminating the transport-of-structure problem that plagues set-theoretic foundations.

The axiom is philosophically radical. It says that mathematical identity is not a primitive metaphysical fact but a structural relationship — two things are the same when they relate to everything else in the same way. This is Leibniz's principle made computational.

Univalence remains technically demanding to implement in proof assistants, but it is the clearest example of a foundational principle that is simultaneously a theorem about structure and a design pattern for mathematics.