Univalence
Overview
Univalence is the principle that the canonical map from type identity to equivalence is itself an equivalence: loosely, structurally equivalent types may be identified. Voevodsky introduced it as the centerpiece of Univalent Foundations (2006–2014), built on Martin-Löf type theory. In the HoTT Book (2013) it is postulated as an axiom alongside the rest of MLTT; in cubical type theories (e.g. CCHM) an analogous statement is often **provable** from the meaning of paths. The community has not settled on a single label “axiom vs theorem”—it depends on the formal system. This archive therefore classifies Univalence as a **framework** (structural layer of univalent mathematics), not as a settled axiom node in the ZFC-style axiom list.
Era: 2006–2013
Proposed at: Princeton, USA (Institute for Advanced Study)
Formal structure
Domain: Universe 𝒰; types A, B : 𝒰; identity type Id_𝒰(A, B) and the type A ≃ B of equivalences
(A =_𝒰 B) ≃ (A ≃ B) (idToEquiv : (A = B) → (A ≃ B) is an equivalence)
Constraints: Book HoTT: primitive postulate. Cubical type theory: typically derived. Status is theory-dependent; not grouped with classical set-theoretic axioms here.
Objective: Equate structural equivalence with identity; support transport, univalent mathematics, and synthetic homotopy without a single global “axiom” classification.