4.8 The object classifier

In type theory we have a basic notion of family of types, namely a function $B:A\to 𝒰$.We have seen that such families behave somewhat like fibrations in homotopy theory, with the fibration being the projection ${\mathrm{𝗉𝗋}}_1:{\sum }_{(a:A)}B(a)\to A$.A basic fact in homotopy theory is that every map is equivalent 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\mathrm{:}A\mathrm{\to }\mathrm{U}$, the fiber of ${\mathrm{pr}}_{\mathrm{1}}\mathrm{:}{\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}B\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\to }A$ over $a\mathrm{:}A$ is equivalent to $B\mathit{}\mathrm{(}a\mathrm{)}$:

$${\mathrm{𝖿𝗂𝖻}}_{{\mathrm{𝗉𝗋}}_1}(a)\simeq B(a)$$

Proof.

We have

${\mathrm{𝖿𝗂𝖻}}_{{\mathrm{𝗉𝗋}}_1}(a)$$:\equiv {\displaystyle \sum _{u:{\sum }_{(x:A)}B(x)}}{\mathrm{𝗉𝗋}}_1(u)=a$

$\simeq {\displaystyle \sum _{(x:A)}}{\displaystyle \sum _{(b:B(x))}}(x=a)$

$\simeq {\displaystyle \sum _{(x:A)}}{\displaystyle \sum _{(p:x=a)}}B(x)$

$\simeq B(a)$

using the left universal property of identity types.∎

Lemma 4.8.2.

For any function $f\mathrm{:}A\mathrm{\to }B$, we have $A\mathrm{\simeq }{\mathrm{\sum }}_{\mathrm{(}b\mathrm{:}B\mathrm{)}}{\mathrm{fib}}_f\mathit{}\mathrm{(}b\mathrm{)}$.

Proof.

We have

${\displaystyle \sum _{b:B}}{\mathrm{𝖿𝗂𝖻}}_f(b)$$:\equiv {\displaystyle \sum _{(b:B)}}{\displaystyle \sum _{(a:A)}}(f(a)=b)$

$\simeq {\displaystyle \sum _{(a:A)}}{\displaystyle \sum _{(b:B)}}(f(a)=b)$

$\simeq A$

using the fact that ${\sum }_{(b:B)}(f(a)=b)$ is contractible.∎

Theorem 4.8.3.

For any type $B$ there is an equivalence

$$\chi :\left(\sum _{A:𝒰}(A\to B)\right)\simeq (B\to 𝒰).$$

Proof.

We have to construct quasi-inverses

$\chi$$:\left({\displaystyle \sum _{A:𝒰}}(A\to B)\right)\to B\to 𝒰$

$\psi$$:(B\to 𝒰)\to \left({\displaystyle \sum _{A:𝒰}}(A\to B)\right).$

We define $\chi$ by $\chi ((A,f),b):\equiv {\mathrm{𝖿𝗂𝖻}}_f(b)$, and $\psi$ by $\psi (P):\equiv (({\sum }_{(b:B)}P(b)),{\mathrm{𝗉𝗋}}_1)$.Now we have to verify that $\chi \circ \psi \sim \mathrm{𝗂𝖽}$ and that $\psi \circ \chi \sim \mathrm{𝗂𝖽}$.

1. Let $P:B\to 𝒰$.By Lemma 4.8.1 (http://planetmath.org/48theobjectclassifier#Thmprelem1),${\mathrm{𝖿𝗂𝖻}}_{{\mathrm{𝗉𝗋}}_1}(b)\simeq P(b)$ for any $b:B$, so it follows immediatelythat $P\sim \chi (\psi (P))$.

2. Let $f:A\to B$ be a function. We have to find a path

   $$({\sum }_{(b:B)}{\mathrm{𝖿𝗂𝖻}}_f(b),{\mathrm{𝗉𝗋}}_1)=(A,f).$$

   First note that by Lemma 4.8.2 (http://planetmath.org/48theobjectclassifier#Thmprelem2), we have$e:{\sum }_{(b:B)}{\mathrm{𝖿𝗂𝖻}}_f(b)\simeq A$ with $e(b,a,p):\equiv a$ and $e^{-1}(a):\equiv (f(a),a,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)})$.By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), it remains to show ${(\mathrm{𝗎𝖺}(e))}_{*}\left({\mathrm{𝗉𝗋}}_1\right)=f$.But by the computation rule for univalence and (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#S0.E3), we have ${(\mathrm{𝗎𝖺}(e))}_{*}\left({\mathrm{𝗉𝗋}}_1\right)={\mathrm{𝗉𝗋}}_1\circ e^{-1}$, and the definition of $e^{-1}$ immediately yields ${\mathrm{𝗉𝗋}}_1\circ e^{-1}\equiv 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 ${𝒰}_{\bullet }$ denotes the type ${\sum }_{(A:𝒰)}A$ of pointed types.

Theorem 4.8.4.

Let $f\mathrm{:}A\mathrm{\to }B$ be a function. Then the diagram

HoTT_fig_4.8.1.png

is a pullback square (see http://planetmath.org/node/87642Exercise 2.11).Here the function ${\vartheta }_f$ is defined by

$$\lambda a.({\mathrm{𝖿𝗂𝖻}}_f(f(a)),(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)})).$$

Proof.

Note that we have the equivalences

$A$$\simeq {\displaystyle \sum _{b:B}}{\mathrm{𝖿𝗂𝖻}}_f(b)$

$\simeq {\displaystyle \sum _{(b:B)}}{\displaystyle \sum _{(X:𝒰)}}{\displaystyle \sum _{(p:{\mathrm{𝖿𝗂𝖻}}_f(b)=X)}}X$

$\simeq {\displaystyle \sum _{(b:B)}}{\displaystyle \sum _{(X:𝒰)}}{\displaystyle \sum _{(x:X)}}{\mathrm{𝖿𝗂𝖻}}_f(b)=X$

$\simeq {\displaystyle \sum _{(b:B)}}{\displaystyle \sum _{(Y:{𝒰}_{\bullet })}}{\mathrm{𝖿𝗂𝖻}}_f(b)={\mathrm{𝗉𝗋}}_{1}Y$

$\equiv B{\times }_{𝒰}{𝒰}_{\bullet }.$

which gives us a composite equivalence $e:A\simeq B{\times }_{𝒰}{𝒰}_{\bullet }$.We may display the action of this composite equivalence step by step by

$a$$\mapsto (f(a),(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)}))$

$\mapsto (f(a),{\mathrm{𝖿𝗂𝖻}}_f(f(a)),{\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝖿𝗂𝖻}}_f(f(a))},(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)}))$

$\mapsto (f(a),{\mathrm{𝖿𝗂𝖻}}_f(f(a)),(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{f(a)}),{\mathrm{𝗋𝖾𝖿𝗅}}_{{\mathrm{𝖿𝗂𝖻}}_f(f(a))}).$

Therefore, we get homotopies $f\sim {\mathrm{𝗉𝗋}}_1\circ e$ and ${\vartheta }_f\sim {\mathrm{𝗉𝗋}}_2\circ e$.∎