Univalence Axiom

Abstract

The Univalence Axiom is the defining principle of Homotopy Type Theory, introduced by Vladimir Voevodsky. 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 $A,B:\mathcal{U}$ in a universe, the canonical map from the type of equivalences to the identity type is itself an equivalence.

Formally, there is a function idtoeqv defined by Path Induction: $idtoeqv:(A=B)\to (A\simeq B)$ which sends the reflexivity path $ref{l}_A$ to the identity equivalence $i{d}_A$. The axiom asserts that $idtoeqv$ is an equivalence: $(A=B)\simeq (A\simeq B)$

Properties

Transport and Substitution

Because $A=B$ implies that any property $P(A)$ holds for $P(B)$, the univalence axiom allows the transport of theorems, structures, and data across any equivalence. If $A\simeq B$, then any property proven for $A$ automatically applies to $B$.

Function Extensionality

In Homotopy Type Theory, the univalence axiom implies Function Extensionality. This principle states that two functions $f,g:A\to B$ are equal if they are pointwise equal: $(\Pi x:A.f(x)=g(x))\to (f=g)$

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-univalent-foundations - Univalent Foundations Program, “Homotopy Type Theory: Univalent Foundations of Mathematics,” Institute for Advanced Study, 2013. voevodsky2010-univalence - V. Voevodsky, “A universe-level axiom of univalence,” 2010. cohen2016-cubical-type-theory - C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, “Cubical Type Theory: a constructive interpretation of the univalence axiom,” 2016.