2.10 Universes and the univalence axiom

Given two types $A$ and $B$ , we may consider them as elements of some universe type $\mathcal{U}$ , and thereby form the identity type $A=_{\mathcal{U}}B$ . As mentioned in the introduction, univalence is the identification of $A=_{\mathcal{U}}B$ with the type $(A\simeq B)$ of equivalences from $A$ to $B$ , which we described in §2.4 (http://planetmath.org/24homotopiesandequivalences). We perform this identification by way of the following canonical function.

Lemma 2.10.1.

For types $A,B:\mathcal{U}$ , there is a certain function,

$\mathsf{idtoeqv}:(A=_{\mathcal{U}}B)\to(A\simeq B),$

(2.10.1)

defined in the proof.

Proof.

We could construct this directly by induction on equality, but the following description is more convenient. Note that the identity function $\mathsf{id}_{\mathcal{U}}:\mathcal{U}\to\mathcal{U}$ may be regarded as a type family indexed by the universe $\mathcal{U}$ ; it assigns to each type $X:\mathcal{U}$ the type $X$ itself. (When regarded as a fibration, its total space is the type $\mathchoice{\sum_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U% })}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}% {\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_% {(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:% \mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:% \mathcal{U})}}}A$ of “pointed types”; see also §4.8 (http://planetmath.org/48theobjectclassifier).) Thus, given a path $p:A=_{\mathcal{U}}B$ , we have a transport function ${p}_{*}:A\to B$ . We claim that ${p}_{*}$ is an equivalence. But by induction, it suffices to assume that $p$ is $\mathsf{refl}_{A}$ , in which case ${p}_{*}\equiv\mathsf{id}_{A}$ , which is an equivalence by Example 2.4.7 (http://planetmath.org/24homotopiesandequivalences#Thmpreeg1). Thus, we can define $\mathsf{idtoeqv}(p)$ to be ${p}_{*}$ (together with the above proof that it is an equivalence). ∎

We would like to say that $\mathsf{idtoeqv}$ is an equivalence. However, as with $\mathsf{happly}$ for function types, the type theory described in http://planetmath.org/node/87533Chapter 1 is insufficient to guarantee this. Thus, as we did for function extensionality, we formulate this property as an axiom: Voevodsky’s univalence axiom.

Axiom 2.10.3 (Univalence).

For any $A,B:\mathcal{U}$ , the function (2.10.1) is an equivalence,

$(A=_{\mathcal{U}}B)\simeq(A\simeq B).$

Technically, the univalence axiom is a statement about a particular universe type $\mathcal{U}$ . If a universe $\mathcal{U}$ satisfies this axiom, we say that it is univalent. Except when otherwise noted (e.g. in §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality)) we will assume that all universes are univalent.

Remark 2.10.4.

It is important for the univalence axiom that we defined $A\simeq B$ using a “good” version of $\mathsf{isequiv}$ as described in §2.4 (http://planetmath.org/24homotopiesandequivalences), rather than (say) as $\mathchoice{\sum_{f:A\to B}\,}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum% _{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}{\mathchoice{{\textstyle% \sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}{% \mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)% }}{\sum_{(f:A\to B)}}}\mathsf{qinv}(f)$ .

In particular, univalence means that equivalent types may be identified. As we did in previous sections, it is useful to break this equivalence into:

•

An introduction rule for ( $A=_{\mathcal{U}}B$ ),

$\mathsf{ua}:({A\simeq B})\to(A=_{\mathcal{U}}B).$

•

The elimination rule, which is $\mathsf{idtoeqv}$ ,

$\mathsf{idtoeqv}\equiv\mathsf{transport}^{X\mapsto X}:(A=_{\mathcal{U}}B)\to(A% \simeq B).$

•

The propositional computation rule,

$\mathsf{transport}^{X\mapsto X}(\mathsf{ua}(f),x)=f(x).$

•

The propositional uniqueness principle: for any $p:A=B$ ,

$p=\mathsf{ua}(\mathsf{transport}^{X\mapsto X}(p)).$

We can also identify the reflexivity, concatenation, and inverses of equalities in the universe with the corresponding operations on equivalences:

	$\displaystyle\mathsf{refl}_{A}$	$\displaystyle=\mathsf{ua}(\mathsf{id}_{A})$
	$\displaystyle\mathsf{ua}(f)\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathsf{ua}(g)$	$\displaystyle=\mathsf{ua}(g\circ f)$
	$\displaystyle\mathord{{\mathsf{ua}(f)}^{-1}}$	$\displaystyle=\mathsf{ua}(f^{-1}).$

The first of these follows because $\mathsf{id}_{A}=\mathsf{idtoeqv}(\mathsf{refl}_{A})$ by definition of $\mathsf{idtoeqv}$ , and $\mathsf{ua}$ is the inverse of $\mathsf{idtoeqv}$ . For the second, if we define $p:\!\!\equiv\mathsf{ua}(f)$ and $q:\!\!\equiv\mathsf{ua}(g)$ , then we have

$\mathsf{ua}(g\circ f)=\mathsf{ua}(\mathsf{idtoeqv}(q)\circ\mathsf{idtoeqv}(p))% =\mathsf{ua}(\mathsf{idtoeqv}(p\cdot q))=p\cdot q$

using Lemma 2.3.9 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem6) and the definition of $\mathsf{idtoeqv}$ . The third is similar.

The following observation, which is a special case of Lemma 2.3.10 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem7), is often useful when applying the univalence axiom.

Lemma 2.10.5.

For any type family $B:A\to\mathcal{U}$ and $x, y : A$ with a path $p:x=y$ and $u:B(x)$ , we have

	$\displaystyle\mathsf{transport}^{B}(p,u)$	$\displaystyle=\mathsf{transport}^{X\mapsto X}(\mathsf{ap}_{B}(p),u)$
		$\displaystyle=\mathsf{idtoeqv}(\mathsf{ap}_{B}(p))(u).$

Title	2.10 Universes and the univalence axiom
\metatable