2.10 Universes and the univalence axiom

Given two types $A$ and $B$, we may consider them as elements of some universe type $𝒰$, and thereby form the identity type $A{=}_{𝒰}B$.As mentioned in the introduction, univalence is the identification of $A{=}_{𝒰}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\mathrm{,}B\mathrm{:}\mathrm{U}$, there is a certain function,

$$\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}:(A{=}_{𝒰}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 ${\mathrm{𝗂𝖽}}_{𝒰}:𝒰\to 𝒰$ may be regarded as a type family indexed by the universe $𝒰$; it assigns to each type $X:𝒰$ the type $X$ itself.(When regarded as a fibration, its total space is the type ${\sum }_{(A:𝒰)}A$ of “pointed types”; see also §4.8 (http://planetmath.org/48theobjectclassifier).)Thus, given a path $p:A{=}_{𝒰}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 ${\mathrm{𝗋𝖾𝖿𝗅}}_A$, in which case $p_{*}\equiv {\mathrm{𝗂𝖽}}_A$, which is an equivalence by Example 2.4.7 (http://planetmath.org/24homotopiesandequivalences#Thmpreeg1).Thus, we can define $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(p)$ to be $p_{*}$ (together with the above proof that it is an equivalence).∎

We would like to say that $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}$ is an equivalence.However, as with $\mathrm{𝗁𝖺𝗉𝗉𝗅𝗒}$ 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\mathrm{,}B\mathrm{:}\mathrm{U}$, the function (2.10.1) is an equivalence,

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

Technically, the univalence axiom is a statement about a particular universe type $𝒰$.If a universe $𝒰$ 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\mathrm{\simeq }B$ using a “good” version of $\mathrm{isequiv}$ as described in §2.4 (http://planetmath.org/24homotopiesandequivalences), rather than (say) as ${\mathrm{\sum }}_{\mathrm{(}f\mathrm{:}A\mathrm{\to }B\mathrm{)}}\mathrm{qinv}\mathit{}\mathrm{(}f\mathrm{)}$.

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{=}_{𝒰}B$),

  $$\mathrm{𝗎𝖺}:(A\simeq B)\to (A{=}_{𝒰}B).$$

• The elimination rule, which is $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}$,

  $$\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}\equiv {\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}:(A{=}_{𝒰}B)\to (A\simeq B).$$

• The propositional computation rule,

  $${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}(\mathrm{𝗎𝖺}(f),x)=f(x).$$

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

  $$p=\mathrm{𝗎𝖺}({\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}(p)).$$

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

${\mathrm{𝗋𝖾𝖿𝗅}}_A$$=\mathrm{𝗎𝖺}({\mathrm{𝗂𝖽}}_A)$

$\mathrm{𝗎𝖺}(f)\mathrm{𝗎𝖺}(g)$$=\mathrm{𝗎𝖺}(g\circ f)$

$\mathrm{𝗎𝖺}{(f)}^{-1}$$=\mathrm{𝗎𝖺}(f^{-1}).$

The first of these follows because ${\mathrm{𝗂𝖽}}_A=\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}({\mathrm{𝗋𝖾𝖿𝗅}}_A)$ by definition of $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}$, and $\mathrm{𝗎𝖺}$ is the inverse of $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}$.For the second, if we define $p:\equiv \mathrm{𝗎𝖺}(f)$ and $q:\equiv \mathrm{𝗎𝖺}(g)$, then we have

$$\mathrm{𝗎𝖺}(g\circ f)=\mathrm{𝗎𝖺}(\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(q)\circ \mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(p))=\mathrm{𝗎𝖺}(\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(p\cdot q))=p\cdot q$$

using Lemma 2.3.9 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem6) and the definition of $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}$.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\mathrm{:}A\mathrm{\to }\mathrm{U}$ and $x\mathrm{,}y\mathrm{:}A$ with a path $p\mathrm{:}x\mathrm{=}y$ and $u\mathrm{:}B\mathit{}\mathrm{(}x\mathrm{)}$, we have

${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^B(p,u)$$={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{X\mapsto X}({\mathrm{𝖺𝗉}}_B(p),u)$

$=\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}({\mathrm{𝖺𝗉}}_B(p))(u).$