# 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)$.

• 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)).$
 $\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