4.8 The object classifier

In type theoryPlanetmathPlanetmath we have a basic notion of family of types, namely a function B:A→𝒰. We have seen that such families behave somewhat like fibrationsMathworldPlanetmath in homotopy theory, with the fibration being the projection 𝗉𝗋1:βˆ‘(a:A)B⁒(a)β†’A. A basic fact in homotopy theory is that every map is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to a fibration. With univalence at our disposal, we can prove the same thing in type theory.

Lemma 4.8.1.

For any type family B:Aβ†’U, the fiber of pr1:βˆ‘(x:A)B⁒(x)β†’A over a:A is equivalent to B⁒(a):


We have

𝖿𝗂𝖻𝗉𝗋1⁒(a) :β‰‘βˆ‘u:βˆ‘(x:A)B⁒(x)𝗉𝗋1(u)=a

using the left universal propertyMathworldPlanetmath of identity types. ∎

Lemma 4.8.2.

For any function f:Aβ†’B, we have Aβ‰ƒβˆ‘(b:B)fibf⁒(b).


We have

βˆ‘b:B𝖿𝗂𝖻f⁒(b) :β‰‘βˆ‘(b:B)βˆ‘(a:A)(f(a)=b)

using the fact that βˆ‘(b:B)(f(a)=b) is contractibleMathworldPlanetmath. ∎

Theorem 4.8.3.

For any type B there is an equivalence


We have to construct quasi-inversesPlanetmathPlanetmath

Ο‡ :(βˆ‘A:𝒰(Aβ†’B))β†’B→𝒰
ψ :(B→𝒰)β†’(βˆ‘A:𝒰(Aβ†’B)).

We define Ο‡ by Ο‡((A,f),b):≑𝖿𝗂𝖻f(b), and ψ by ψ(P):≑((βˆ‘(b:B)P(b)),𝗉𝗋1). Now we have to verify that Ο‡βˆ˜ΟˆβˆΌπ—‚π–½ and that Οˆβˆ˜Ο‡βˆΌπ—‚π–½.

  1. 1.

    Let P:B→𝒰. By Lemma 4.8.1 (http://planetmath.org/48theobjectclassifier#Thmprelem1), 𝖿𝗂𝖻𝗉𝗋1⁒(b)≃P⁒(b) for any b:B, so it follows immediately that PβˆΌΟ‡β’(ψ⁒(P)).

  2. 2.

    Let f:A→B be a function. We have to find a path


    First note that by Lemma 4.8.2 (http://planetmath.org/48theobjectclassifier#Thmprelem2), we have e:βˆ‘(b:B)𝖿𝗂𝖻f⁒(b)≃A with e(b,a,p):≑a and e-1(a):≑(f(a),a,𝗋𝖾𝖿𝗅f⁒(a)). By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), it remains to show (π—Žπ–Ί(e))*(𝗉𝗋1)=f. But by the computation rule for univalence andΒ (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#S0.E3), we have (π—Žπ–Ί(e))*(𝗉𝗋1)=𝗉𝗋1∘e-1, and the definition of e-1 immediately yields 𝗉𝗋1∘e-1≑f.∎

In particular, this implies that we have an object classifier in the sense of higher topos theory. Recall from Definition 2.1.7 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn1) that π’°βˆ™ denotes the type βˆ‘(A:𝒰)A of pointed types.

Theorem 4.8.4.

Let f:A→B be a function. Then the diagram



is a pullback square (see http://planetmath.org/node/87642Exercise 2.11). Here the function Ο‘f is defined by


Note that we have the equivalences

A β‰ƒβˆ‘b:B𝖿𝗂𝖻f⁒(b)

which gives us a composite equivalence e:A≃BΓ—π’°π’°βˆ™. We may display the action of this composite equivalence step by step by

a ↦(f(a),(a,𝗋𝖾𝖿𝗅f⁒(a)))

Therefore, we get homotopiesMathworldPlanetmath fβˆΌπ—‰π—‹1∘e and Ο‘fβˆΌπ—‰π—‹2∘e. ∎

Title 4.8 The object classifier