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.
For types , there is a certain function,
defined in the 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.
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 .
An introduction rule for (),
The elimination rule, which is ,
The propositional computation rule,
The propositional uniqueness principle: for any ,
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.
For any type family and with a path and , we have
|Title||2.10 Universes and the univalence axiom|