2.10 Universes and the univalence axiom

Given two types A and B, we may consider them as elements of some universePlanetmathPlanetmath 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≃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:U, there is a certain function,

π—‚π–½π—π—ˆπ–Ύπ—Šπ—:(A=𝒰B)β†’(A≃B), (2.10.1)

defined in the proof.


We could construct this directly by inductionMathworldPlanetmath 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 X:𝒰 the type X itself. (When regarded as a fibrationMathworldPlanetmath, its total space is the type βˆ‘(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β†’B. We claim that p* is an equivalence. But by induction, it suffices to assume that p is 𝗋𝖾𝖿𝗅A, in which case p*≑𝗂𝖽A, which is an equivalence by Example 2.4.7 (http://planetmath.org/24homotopiesandequivalences#Thmpreeg1). Thus, we can define π—‚π–½π—π—ˆπ–Ύπ—Šπ—β’(p) to be p* (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 theoryPlanetmathPlanetmath 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:U, 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 A≃B using a β€œgood” version of isequiv as described in Β§2.4 (http://planetmath.org/24homotopiesandequivalences), rather than (say) as βˆ‘(f:Aβ†’B)qinv⁒(f).

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

  • β€’

    An introduction rule for (A=𝒰B),

  • β€’

    The elimination rule, which is π—‚π–½π—π—ˆπ–Ύπ—Šπ—,

  • β€’

    The propositional computation rule,

  • β€’

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


We can also identify the reflexivityMathworldPlanetmath, concatenationMathworldPlanetmath, and inversesPlanetmathPlanetmathPlanetmath of equalities in the universe with the corresponding operationsMathworldPlanetmath on equivalences:

𝗋𝖾𝖿𝗅A =π—Žπ–Ίβ’(𝗂𝖽A)
π—Žπ–Ίβ’(f)⁒\centerdotβ’π—Žπ–Ίβ’(g) =π—Žπ–Ίβ’(g∘f)
π—Žπ–Ίβ’(f)-1 =π—Žπ–Ίβ’(f-1).

The first of these follows because 𝗂𝖽A=π—‚π–½π—π—ˆπ–Ύπ—Šπ—β’(𝗋𝖾𝖿𝗅A) by definition of π—‚π–½π—π—ˆπ–Ύπ—Šπ—, and π—Žπ–Ί is the inverse of π—‚π–½π—π—ˆπ–Ύπ—Šπ—. For the second, if we define p:β‰‘π—Žπ–Ί(f) and q:β‰‘π—Žπ–Ί(g), 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 B:Aβ†’U and x,y:A with a path p:x=y and u:B⁒(x), we have

π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—B⁒(p,u) =π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—X↦X⁒(𝖺𝗉B⁒(p),u)
Title 2.10 Universes and the univalence axiom