nLab
univalence axiom

Idea

In intensional type theory, identity types behave like path space objects; this viewpoint is called homotopy type theory. This induces furthermore a notion of homotopy fibers, hence of homotopy equivalences between types.

On the other hand, if type theory contains a universe Type, so that types can be considered as points of $\mathrm{Type}$, then between two types we also have an identity type ${\mathrm{Paths}}_{\mathrm{Type}}(X,Y)$. The univalence axiom says that these two notions of “sameness” for types are the same. Morally, this says that Type behaves like an object classifier.

The name univalence (due to Voevodsky) comes from the following reasoning. A fibration or bundle $p:E\to B$ of some sort is commonly said to be universal if every other bundle of the same sort is a pullback of $p$ in a unique way (up to homotopy). Less commonly, a bundle is said to be versal if every other bundle is a pullback of it in some way, not necessarily unique. By contrast, a bundle is said to be univalent if every other bundle is a pullback of it in at most one way (up to homotopy). The univalence axiom then says that the canonical fibration over $\mathrm{Type}$ is univalent, for every fibration with small fibers is an essentially unique pullback of this one (while those with large fibers are not, they are pullbacks of the next higher ${\mathrm{Type}}_1$).

Definition

We state univalence first in (intensional) type theory and then in its categorical semantics.

In the type theory

Let $X$ and $Y$ be types. There is a canonically defined map from the identity type $(X=Y)$ of paths (in Type) between them to the function type $(X\stackrel{\simeq }{\to }Y)$ of equivalences in homotopy type theory between them. It can be defined by path induction, i.e. the eliminator for the identity types, by specifying that it takes the identity path $1_X:(X=X)$ to the identity equivalence of $X$.

Univalence: For any two types $X,Y$, this map $(X=Y)\to (X\simeq Y)$ is an equivalence.

Univalence is a commonly assumed axiom in homotopy type theory, and is central to the proposal (Voevodsky) that this provides a natively homotopy theoretic foundation of mathematics (the Univalent Foundations Project.)

In categorical semantics

Let $𝒞$ be a locally cartesian closed model category in which all objects are cofibrant.

By the categorical semantics of homotopy type theory, a dependent type

$$b:B⊢E(b):\mathrm{Type}$$b : B \vdash E(b) : Type

corresponds to a morphism $E\to B$ in $𝒞$ that is a fibration between fibrant objects.

Then the dependent function type

$$b_1,b_2:B⊢(E(b_1)\to E(b_2)):\mathrm{Type}$$b_1, b_2 : B \vdash ( E(b_1) \to E(b_2)) : Type

is interpreted as the internal hom $[-,-{]}_{𝒞{/}_{B\times B}}$ in the slice category $𝒞{/}_{B\times B}$ after extending $E$ to the context $B\times B$ by pulling back along the two projections $p_1,p_2:B\times B\to B$, respectively. Hence this is interpreted as

$$[p_1^{*}E,p_2^{*}E{]}_{𝒞{/}_{B\times B}}\simeq [E\times B,B\times E{]}_{𝒞{/}_{B\times B}}\in 𝒞{/}_{B\times B}.$$[p_1^* E \, , \, p_2^* E]_{\mathcal{C}/_{B \times B}} \simeq [E \times B \, , \, B \times E]_{\mathcal{C}/_{B \times B}} \in \mathcal{C}/_{B \times B} \,.

Consider then the diagonal morphism ${\Delta }_B:B\to B\times B$ in $𝒞$ as an object of $𝒞{/}_{B\times B}$. We would like to define a morphism

$$q:{\Delta }_B\to [E\times B,B\times E{]}_{𝒞{/}_{B\times B}}.$$q \colon \Delta_B \to [E \times B , B \times E]_{\mathcal{C}/_{B \times B}} \,.

in $𝒞{/}_{B\times B}$. By the defining (product $⊣$ internal hom)-adjunction, it suffices to define a morphism

$${\Delta }_B{\times }_{𝒞{/}_{B\times B}}E\times B\to B\times E$$\Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B \to B \times E

in $𝒞{/}_{B\times B}$. But now by the universal property of pullback, it suffices to define just in ${𝒞}_{/B}$ a morphism

$${\Delta }_B{\times }_{𝒞{/}_{B\times B}}E\times B\to {\Delta }_B{\times }_{𝒞{/}_{B\times B}}B\times E.$$\Delta_B \times_{\mathcal{C}/_{B \times B}} E \times B \to \Delta_B \times_{\mathcal{C}/_{B \times B}} B \times E\,.

And since the composite pullback along either composite

$$B\stackrel{{\Delta }_B}{\to }B\times B\stackrel{{\pi }_1}{\to }B$$B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_1} B

$$B\stackrel{{\Delta }_B}{\to }B\times B\stackrel{{\pi }_2}{\to }B$$B \xrightarrow{\Delta_B} B\times B \xrightarrow{\pi_2} B

is the identity, both ${\Delta }_B{\times }_{𝒞{/}_{B\times B}}E\times B$ and ${\Delta }_B{\times }_{𝒞{/}_{B\times B}}B\times E$ are isomorphic to $E$; thus here we can take the identity morphism.

Now, using the path object factorization in $𝒞$

$$\begin{array}{ccccc}B& & \stackrel{\simeq }{\hookrightarrow }& & B^I\\ & {}_{{\Delta }_B}\searrow & & {\swarrow }_{}\\ & & B\times B\end{array}$$\array{ B &&\stackrel{\simeq}{\hookrightarrow}&& B^I \\ & {}_{\mathllap{\Delta_B}}\searrow && \swarrow_{\mathrlap{}} \\ && B \times B }

by an acyclic cofibration followed by a fibration, we obtain a fibrant replacement of ${\Delta }_B$ in the slice model category ${𝒞}_{B\times B}$.

Since also $[E\times B,B\times E{]}_{𝒞{/}_{B\times B}}$ is fibrant by the axioms on the locally cartesian closed model category $𝒞$, we have a lift $\hat{q}$ in the diagram in $𝒞{/}_{B\times B}$

$$\begin{array}{ccc}B& \stackrel{q}{\to }& [E\times B,B\times E{]}_{𝒞{/}_{B\times B}}\\ \downarrow & {}^{\hat{q}}\nearrow & \downarrow \\ B^I& \to & B\times B={*}_{𝒞{/}_{B\times B}}\end{array}.$$\array{ B &\stackrel{q}{\to}& [E \times B, B \times E]_{\mathcal{C}/_{B \times B}} \\ \downarrow &{}^{\mathllap{\hat q}}\nearrow& \downarrow \\ B^I &\to& B \times B = *_{\mathcal{C}/_{B \times B}} } \,.

This lift is the interpretation of the path induction that deduces a map on all paths $\gamma \in B^I$ from one on just the identity paths ${\mathrm{id}}_b\in B\hookrightarrow B^I$.

Finally, let $\mathrm{Eq}(E)\hookrightarrow [E\times B,B\times E{]}_{𝒞{/}_{B\times B}}$ be the subobject on the weak equivalences (…), and observe that $q$ and $\hat{q}$ factor through this to give a morphism

$$\hat{q}:B^I\to \mathrm{Eq}(E).$$\hat q : B^I \to Eq(E) \,.

The fibration $E\to B$ is univalent in $𝒞$ if this morphism is a weak equivalence. By the 2-out-of-3 property, of course, it is equivalent to ask that $q:B\to \mathrm{Eq}(E)$ be a weak equivalence.

(…)

In simplicial sets

We specialize the general discussion above to the realization in $𝒞=$ sSet, equipped with the standard model structure on simplicial sets.

For $E\to X$ any fibration (Kan fibration) between fibrant objects (Kan complexes), consider first the simplicial set

$$[E\times B,B\times E{]}_{B\times B}\in \mathrm{sSet}{/}_{B\times B}$$[E \times B , B \times E]_{B \times B} \in sSet/_{B \times B}

defined as the internal hom in the slice category $\mathrm{sSet}{/}_{B\times B}$.

Notice that the vertices of this simplicial set over a fixed pair $(b_1,b_2):*\to B\times B$ of vertices in $B$ form the set of morphisms $E_{b_1}\to E_{b_2}$ between the fibers in $\mathrm{sSet}$.

This is because – by the defining property of the internal hom in the slice and using that products in $\mathrm{sSet}{/}_{B\times B}$ are pullbacks in $\mathrm{sSet}$ – the horizontal morphisms of simplcial sets in

$$\begin{array}{ccccc}*& & \to & & [E\times B,B\times E{]}_{B\times B}\\ & {}_{(b_1,b_2)}\searrow & & \swarrow \\ & & B\times B\end{array}$$\array{ * &&\to&& [E \times B, B \times E]_{B \times B} \\ & {}_{\mathllap{(b_1,b_2)}}\searrow && \swarrow \\ && B \times B }

correspond bijectively to the horizontal morphisms in

$$\begin{array}{ccccc}{E}_{b_1}\times \{b_2\}& & \to & & \{b_1\}\times E_{b_2}\\ & \searrow & & \swarrow \\ & & B\times B\end{array}$$\array{ E_{b_1} \times \{b_2\} &&\to&& \{b_1\} \times E_{b_2} \\ & \searrow && \swarrow \\ && B \times B }

in $\mathrm{sSet}$, which are precisely morphisms $E_{b_1}\to E_{b_2}$.

Let then

$$\mathrm{Eq}(E)\hookrightarrow [E\times B,B\times E{]}_{B\times B}\in \mathrm{sSet}{/}_{B\times B}$$Eq(E) \hookrightarrow [E \times B, B \times E]_{B \times B} \in sSet/_{B \times B}

be the full sub-simplicial set on those vertices that correspond to weak equivalences ((weak) homotopy equivalences).

By a similar consideration, one sees that the diagonal morphism ${\Delta }_B:B\to B\times B$ in $\mathrm{sSet}$, regarded as an object $B\in \mathrm{sSet}{/}_{B\times B}$, comes with a canonical morphism

$$B\to \mathrm{Eq}(E).$$B \to Eq(E) \,.

The fibration $E\to B$ is univalent, precisely when this morphism is a weak equivalence.

This appears originally as Voevodsky, def. 3.4

In simplicial presheaves

(…)

Properties

The univalence axiom implies function extensionality.

A commented version of a formal proof of this fact can be found in (Bauer-Lumsdaine).

Related concepts

Univalence is essentially the same as the “completeness” condition in the theory of Segal spaces/semi-Segal spaces. See at complete Segal space/_complete semi-Segal space_.

References

The univalence axiom was introduced and promoted by Vladimir Voevodsky around 2005. (?)

• Vladimir Voevodsky, Univalent Foundations Project (pdf)

A quick survey is for instance in

• Peter Aczel, On Voevodsky’s univalence axiom (pdf)

An exposition is at

• Mike Shulman, Homotopy type theory, IV (blog post)

An accessible account of Voevodsky’s proof that the universal Kan fibration in simplicial sets is univalent is at

• Chris Kapulkin, Peter LeFanu Lumsdaine, Vladimir Voevodsky, Univalence in simplicial sets, arXiv

A quick elegant proof of the object classifier/universal associated infinity-bundle in simplicial sets/$\mathrm{\infty }$-groupoids is in

• Ieke Moerdijk (notes by Chris Kapulkin), Fiber bundles and univalence (pdf)

The HoTT-Coq code is at

• HoTT/Coq/Univalence.v

• HoTT/Coq/UnivalenceAxiom.v

A guided walk through the formal proof that univalence implies functional extensionality is at

• Andrej Bauer, Peter LeFanu Lumsdaine, Oberwolfach HoTT-Coq tutorial

A discussion of univalence in categories of presheaves over an inverse category with values in a category for which univalence is already established is discussed in

• Michael Shulman, The univalence axiom for inverse diagrams (arXiv:1203.3253)

The computational interpretation of univalence / canonicity is discussed in

• Dan Licata, Robert Harper, Computing with Univalence (2012) (pdf)

• Robert Harper, Daniel Licata, Canonicity for 2-dimensional type theory (2011) (pdf)

• Daniel Licata The computational interpretation of HoTT (in 2D), talk at UF-IAS-2012 (video)

• Simon Huber (with Thierry Coquand), Towards a computational justification of the Axiom of Univalence , talk at TYPES 2011 (pdf)

• Bruno Barras, Thierry Coquand, Simon Huber, A Generalization of Takeuti-Gandy Interpretation (pdf)

Univalence is claimed to be established in all (infinity,1)-toposes, their presentations by type-theoretic model categories as well as further cases of locally cartesian closed (infinity,1)-categories in

• David Gepner, Joachim Kock, Univalence in locally cartesian closed infinity-categories (arXiv:1208.1749)

For more references see homotopy type theory.