2.10 Universes and the univalence axiom
Given two types and , we may consider them as elements of some universe type , and thereby form the identity type .
As mentioned in the introduction, univalence is the identification of with the type of equivalences from to , 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 , there is a certain function,
(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 may be regarded as a type family indexed by the universe ; it assigns to each type the type itself.
(When regarded as a fibration
, its total space is the type of βpointed typesβ; see also Β§4.8 (http://planetmath.org/48theobjectclassifier).)
Thus, given a path , we have a transport function .
We claim that is an equivalence.
But by induction, it suffices to assume that is , in which case , which is an equivalence by Example 2.4.7 (http://planetmath.org/24homotopiesandequivalences#Thmpreeg1).
Thus, we can define to be (together with the above proof that it is an equivalence).
β
We would like to say that is an equivalence.
However, as with 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 , the functionΒ (2.10.1) is an equivalence,
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 using a βgoodβ version of as described in Β§2.4 (http://planetmath.org/24homotopiesandequivalences), rather than (say) as .
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 (),
-
β’
The elimination rule, which is ,
-
β’
The propositional computation rule,
-
β’
The propositional uniqueness principle: for any ,
We can also identify the reflexivity, concatenation
, and inverses
of equalities in the universe with the corresponding operations
on equivalences:
The first of these follows because by definition of , and is the inverse of . For the second, if we define and , then we have
using Lemma 2.3.9 (http://planetmath.org/23typefamiliesarefibrations#Thmprelem6) and the definition of . 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 and with a path and , we have
Title | 2.10 Universes and the univalence axiom |
\metatable |