4.8 The object classifier

In type theory  we have a basic notion of family of types, namely a function $B:A\to\mathcal{U}$. We have seen that such families behave somewhat like fibrations  in homotopy theory, with the fibration being the projection $\mathsf{pr}_{1}:\mathchoice{\sum_{a:A}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}% }{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A% )}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(% a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\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:A\to\mathcal{U}$, the fiber of $\mathsf{pr}_{1}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}% }{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x)\to A$ over $a:A$ is equivalent to $B(a)$:

 ${\mathsf{fib}}_{\mathsf{pr}_{1}}(a)\simeq B(a)$
Proof.

We have

 $\displaystyle{\mathsf{fib}}_{\mathsf{pr}_{1}}(a)$ $\displaystyle:\!\!\equiv\mathchoice{\sum_{u:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x)}\,}{\mathchoice{{\textstyle\sum_{(u:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x))}}}{\sum_{(u:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}B(x))}}{\sum_{(u:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum% _{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{\sum_{(u:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\mathchoice{{\textstyle\sum_{(u:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\sum_{(u:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}B(x))}}{\sum_{(u:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum% _{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}{% \sum_{(u:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_% {(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\mathchoice{{\textstyle% \sum_{(u:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_% {(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}{\sum_{(u:\mathchoice{% \sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}% }{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:% A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{% (x:A)}}{\sum_{(x:A)}}}B(x))}}{\sum_{(u:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}B(x))}}{\sum_{(u:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum% _{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}B(x))}}}\mathsf{pr}_{% 1}(u)=a$ $\displaystyle\simeq\mathchoice{\sum_{(x:A)}\,}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}\mathchoice{\sum_{(b:% B(x))}\,}{\mathchoice{{\textstyle\sum_{(b:B(x))}}}{\sum_{(b:B(x))}}{\sum_{(b:B% (x))}}{\sum_{(b:B(x))}}}{\mathchoice{{\textstyle\sum_{(b:B(x))}}}{\sum_{(b:B(x% ))}}{\sum_{(b:B(x))}}{\sum_{(b:B(x))}}}{\mathchoice{{\textstyle\sum_{(b:B(x))}% }}{\sum_{(b:B(x))}}{\sum_{(b:B(x))}}{\sum_{(b:B(x))}}}(x=a)$ $\displaystyle\simeq\mathchoice{\sum_{(x:A)}\,}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}\mathchoice{\sum_{(p:% x=a)}\,}{\mathchoice{{\textstyle\sum_{(p:x=a)}}}{\sum_{(p:x=a)}}{\sum_{(p:x=a)% }}{\sum_{(p:x=a)}}}{\mathchoice{{\textstyle\sum_{(p:x=a)}}}{\sum_{(p:x=a)}}{% \sum_{(p:x=a)}}{\sum_{(p:x=a)}}}{\mathchoice{{\textstyle\sum_{(p:x=a)}}}{\sum_% {(p:x=a)}}{\sum_{(p:x=a)}}{\sum_{(p:x=a)}}}B(x)$ $\displaystyle\simeq B(a)$
Lemma 4.8.2.

For any function $f:A\to B$, we have $A\simeq\mathchoice{\sum_{b:B}\,}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(% b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum% _{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{% \sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathsf{fib}}_{f}(b)$.

Proof.

We have

 $\displaystyle\mathchoice{\sum_{b:B}\,}{\mathchoice{{\textstyle\sum_{(b:B)}}}{% \sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}% }}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:% B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathsf{fib}}_{f}(b)$ $\displaystyle:\!\!\equiv\mathchoice{\sum_{(b:B)}\,}{\mathchoice{{\textstyle% \sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{% \textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{% \mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}% }}\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A% )}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(% a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum% _{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}(f(a)=b)$ $\displaystyle\simeq\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a% :A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_% {(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle% \sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice{\sum_{(b:% B)}\,}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_% {(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{% \sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)% }}{\sum_{(b:B)}}}(f(a)=b)$ $\displaystyle\simeq A$

using the fact that $\mathchoice{\sum_{b:B}\,}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{% \sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)% }}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b% :B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}(f(a)=b)$ is contractible  . ∎

Theorem 4.8.3.

For any type $B$ there is an equivalence

 $\chi:\Bigl{(}\mathchoice{\sum_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\sum_{% (A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:% \mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{% \textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U% })}}{\sum_{(A:\mathcal{U})}}}(A\to B)\Bigr{)}\simeq(B\to\mathcal{U}).$
Proof.
 $\displaystyle\chi$ $\displaystyle:\Bigl{(}\mathchoice{\sum_{A:\mathcal{U}}\,}{\mathchoice{{% \textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U% })}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{% \sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{% \mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{% (A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}(A\to B)\Bigr{)}\to B\to\mathcal{U}$ $\displaystyle\psi$ $\displaystyle:(B\to\mathcal{U})\to\Bigl{(}\mathchoice{\sum_{A:\mathcal{U}}\,}{% \mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{% (A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:% \mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:% \mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}(A\to B)\Bigr{)}.$

We define $\chi$ by $\chi((A,f),b):\!\!\equiv{\mathsf{fib}}_{f}(b)$, and $\psi$ by $\psi(P):\!\!\equiv{\mathopen{}\left((\mathchoice{\sum_{b:B}\,}{\mathchoice{{% \textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{% \mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}% }}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:% B)}}}P(b)),\mathsf{pr}_{1}\right)\mathclose{}}$. Now we have to verify that $\chi\circ\psi\sim\mathsf{id}{}$ and that $\psi\circ\chi\sim\mathsf{id}{}$.

1. 1.

Let $P:B\to\mathcal{U}$. By Lemma 4.8.1 (http://planetmath.org/48theobjectclassifier#Thmprelem1), ${\mathsf{fib}}_{\mathsf{pr}_{1}}(b)\simeq P(b)$ for any $b:B$, so it follows immediately that $P\sim\chi(\psi(P))$.

2. 2.

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

 ${\mathopen{}\left(\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b% :B)}}{\sum_{(b:B)}}{\mathsf{fib}}_{f}(b),\,\mathsf{pr}_{1}\right)\mathclose{}}% ={\mathopen{}(A,f)\mathclose{}}.$

First note that by Lemma 4.8.2 (http://planetmath.org/48theobjectclassifier#Thmprelem2), we have $e:\mathchoice{\sum_{b:B}\,}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:B)}% }{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{(b:% B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(b:B)}}}{\sum_{% (b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathsf{fib}}_{f}(b)\simeq A$ with $e(b,a,p):\!\!\equiv a$ and $e^{-1}(a):\!\!\equiv(f(a),a,\mathsf{refl}_{f(a)})$. By Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), it remains to show ${(\mathsf{ua}(e))}_{*}\mathopen{}\left({\mathsf{pr}_{1}}\right)\mathclose{}=f$. But by the computation rule for univalence and (2.9.4) (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom#S0.E3), we have ${(\mathsf{ua}(e))}_{*}\mathopen{}\left({\mathsf{pr}_{1}}\right)\mathclose{}=% \mathsf{pr}_{1}\circ e^{-1}$, and the definition of $e^{-1}$ immediately yields $\mathsf{pr}_{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 $\mathcal{U}_{\bullet}$ denotes the type $\mathchoice{\sum_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U% })}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}% {\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_% {(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:% \mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:% \mathcal{U})}}}A$ of pointed types.

Theorem 4.8.4.

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

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

 ${\lambda}a.\,{\mathopen{}({\mathsf{fib}}_{f}(f(a)),{\mathopen{}(a,\mathsf{refl% }_{f(a)})\mathclose{}})\mathclose{}}.$
Proof.

Note that we have the equivalences

 $\displaystyle A$ $\displaystyle\simeq\mathchoice{\sum_{b:B}\,}{\mathchoice{{\textstyle\sum_{(b:B% )}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_{(% b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum% _{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathsf{fib}}_{f}(b)$ $\displaystyle\simeq\mathchoice{\sum_{(b:B)}\,}{\mathchoice{{\textstyle\sum_{(b% :B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_% {(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle% \sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}\mathchoice{\sum_{(X:% \mathcal{U})}\,}{\mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:% \mathcal{U})}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}{\mathchoice{{% \textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U% })}}{\sum_{(X:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{% \sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}% \mathchoice{\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}\,}{\mathchoice{{\textstyle\sum_% {(p:{\mathsf{fib}}_{f}(b)=X)}}}{\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}}{\sum_{(p:{% \mathsf{fib}}_{f}(b)=X)}}{\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}}}{\mathchoice{{% \textstyle\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}}}{\sum_{(p:{\mathsf{fib}}_{f}(b)=% X)}}{\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}}{\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}}}{% \mathchoice{{\textstyle\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}}}{\sum_{(p:{\mathsf{% fib}}_{f}(b)=X)}}{\sum_{(p:{\mathsf{fib}}_{f}(b)=X)}}{\sum_{(p:{\mathsf{fib}}_% {f}(b)=X)}}}X$ $\displaystyle\simeq\mathchoice{\sum_{(b:B)}\,}{\mathchoice{{\textstyle\sum_{(b% :B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_% {(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle% \sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}\mathchoice{\sum_{(X:% \mathcal{U})}\,}{\mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:% \mathcal{U})}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}{\mathchoice{{% \textstyle\sum_{(X:\mathcal{U})}}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U% })}}{\sum_{(X:\mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(X:\mathcal{U})}}}{% \sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}{\sum_{(X:\mathcal{U})}}}% \mathchoice{\sum_{(x:X)}\,}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)}% }{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:% X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{% (x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}}{\mathsf{fib}}_{f}(b)=X$ $\displaystyle\simeq\mathchoice{\sum_{(b:B)}\,}{\mathchoice{{\textstyle\sum_{(b% :B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle\sum_% {(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}{\mathchoice{{\textstyle% \sum_{(b:B)}}}{\sum_{(b:B)}}{\sum_{(b:B)}}{\sum_{(b:B)}}}\mathchoice{\sum_{(Y:% \mathcal{U}_{\bullet})}\,}{\mathchoice{{\textstyle\sum_{(Y:\mathcal{U}_{% \bullet})}}}{\sum_{(Y:\mathcal{U}_{\bullet})}}{\sum_{(Y:\mathcal{U}_{\bullet})% }}{\sum_{(Y:\mathcal{U}_{\bullet})}}}{\mathchoice{{\textstyle\sum_{(Y:\mathcal% {U}_{\bullet})}}}{\sum_{(Y:\mathcal{U}_{\bullet})}}{\sum_{(Y:\mathcal{U}_{% \bullet})}}{\sum_{(Y:\mathcal{U}_{\bullet})}}}{\mathchoice{{\textstyle\sum_{(Y% :\mathcal{U}_{\bullet})}}}{\sum_{(Y:\mathcal{U}_{\bullet})}}{\sum_{(Y:\mathcal% {U}_{\bullet})}}{\sum_{(Y:\mathcal{U}_{\bullet})}}}{\mathsf{fib}}_{f}(b)=% \mathsf{pr}_{1}Y$ $\displaystyle\equiv B\times_{\mathcal{U}}\mathcal{U}_{\bullet}.$

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

 $\displaystyle a$ $\displaystyle\mapsto{\mathopen{}(f(a),\;{\mathopen{}(a,\mathsf{refl}_{f(a)})% \mathclose{}})\mathclose{}}$ $\displaystyle\mapsto{\mathopen{}(f(a),\;{\mathsf{fib}}_{f}(f(a)),\;\mathsf{% refl}_{{\mathsf{fib}}_{f}(f(a))},\;{\mathopen{}(a,\mathsf{refl}_{f(a)})% \mathclose{}})\mathclose{}}$ $\displaystyle\mapsto{\mathopen{}(f(a),\;{\mathsf{fib}}_{f}(f(a)),\;{\mathopen{% }(a,\mathsf{refl}_{f(a)})\mathclose{}},\;\mathsf{refl}_{{\mathsf{fib}}_{f}(f(a% ))})\mathclose{}}.$

Therefore, we get homotopies  $f\sim\mathsf{pr}_{1}\circ e$ and $\vartheta_{f}\sim\mathsf{pr}_{2}\circ e$. ∎

Title 4.8 The object classifier
\metatable