Idea
The Univalence Principle or univalence axiom is the defining principle of homotopy type theory, introduced by Vladimir Voevodsky, and used as the basis for the Univalent Foundations Program. It characterizes the Identity Type of the universe of types, asserting that equivalent types are equal. This axiom provides a formal justification for the common mathematical practice of treating isomorphic structures as identical.
Definition
The Univalence Axiom states that for any two types in a universe, the canonical map from the type of equivalence to the identity type is itself an equivalence.
Formally, there is a function idtoeqv defined by Path Induction:
which sends the reflexivity path to the identity equivalence . The axiom asserts that is an equivalence:
Properties
Transport and Substitution
Because implies that any property holds for , the univalence axiom allows the transport of theorems, structures, and data across any equivalence. If , then any property proven for automatically applies to .
Function Extensionality
In Homotopy Type Theory, the univalence axiom implies Function Extensionality. This principle states that two functions are equal if they are pointwise equal:
Computation and Cubical Type Theory
In standard Martin-Löf Type Theory, the univalence axiom is added as an axiom, which blocks the computational reduction (canonicity) of terms. Cubical Type Theory was developed to provide a constructive interpretation where univalence has computational content, allowing for the evaluation of programs that use the axiom.
Related Concepts
- Equivalence: The type-theoretic notion of isomorphism
- Identity Type: The type of paths between terms
- Hierarchy of Types: The classification of types by homotopy level
- Cubical Type Theory: A system with computational univalence
References
hott2013-book voevodsky2010-univalence cohen2016-cubical-type-theory