# 7.6 Orthogonal factorization

In set theory, the surjections and the injections form a unique factorization system: every function factors essentially uniquely as a surjection followed by an injection. We have seen that surjections generalize naturally to $n$-connected maps, so it is natural to inquire whether these also participate in a factorization system. Here is the corresponding generalization of injections.

###### Definition 7.6.1.

A function $f:A\to B$ is $n$-truncated if the fiber ${\mathsf{fib}}_{f}(b)$ is an $n$-type for all $b:B$.

In particular, $f$ is $(-2)$-truncated if and only if it is an equivalence. And of course, $A$ is an $n$-type if and only if $A\to\mathbf{1}$ is $n$-truncated. Moreover, $n$-truncated maps could equivalently be defined recursively, like $n$-types.

###### Lemma 7.6.2.

For any $n\geq-2$, a function $f:A\to B$ is $(n+1)$-truncated if and only if for all $x,y:A$, the map $\mathsf{ap}_{f}:(x=y)\to(f(x)=f(y))$ is $n$-truncated. In particular, $f$ is $(-1)$-truncated if and only if it is an embedding in the sense of Β§4.6 (http://planetmath.org/46surjectionsandembeddings).

###### Proof.

Note that for any $(x,p),(y,q):{\mathsf{fib}}_{f}(b)$, we have

 $\displaystyle\big{(}(x,p)=(y,q)\big{)}$ $\displaystyle=\mathchoice{\sum_{r:x=y}\,}{\mathchoice{{\textstyle\sum_{(r:x=y)% }}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}}{\mathchoice{{\textstyle% \sum_{(r:x=y)}}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}}{\mathchoice{% {\textstyle\sum_{(r:x=y)}}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}}(p% =\mathsf{ap}_{f}(r)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q)$ $\displaystyle=\mathchoice{\sum_{r:x=y}\,}{\mathchoice{{\textstyle\sum_{(r:x=y)% }}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}}{\mathchoice{{\textstyle% \sum_{(r:x=y)}}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}}{\mathchoice{% {\textstyle\sum_{(r:x=y)}}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}{\sum_{(r:x=y)}}}(% \mathsf{ap}_{f}(r)=p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathord{{q}^{-1}})$ $\displaystyle={\mathsf{fib}}_{\mathsf{ap}_{f}}(p\mathchoice{\mathbin{\raisebox% {2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}% }}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{q}^{-1}}).$

Thus, any path space in any fiber of $f$ is a fiber of $\mathsf{ap}_{f}$. On the other hand, choosing $b:\!\!\equiv f(y)$ and $q:\!\!\equiv\mathsf{refl}_{f(y)}$ we see that any fiber of $\mathsf{ap}_{f}$ is a path space in a fiber of $f$. The result follows, since $f$ is $(n+1)$-truncated if all path spaces of its fibers are $n$-types. β

We can now construct the factorization, in a fairly obvious way.

###### Definition 7.6.3.

Let $f:A\to B$ be a function. The $n$-image of $f$ is defined as

 $\mathsf{im}_{n}(f):\!\!\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)}% }}\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{}.$

When $n=-1$, we write simply $\mathsf{im}(f)$ and call it the image of $f$.

###### Lemma 7.6.4.

For any function $f:A\to B$, the canonical function $\tilde{f}:A\to\mathsf{im}_{n}(f)$ is $n$-connected. Consequently, any function factors as an $n$-connected function followed by an $n$-truncated function.

###### Proof.

Note that $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)$. The function $\tilde{f}$ is the function on total spaces induced by the canonical fiberwise transformation

 $\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(b:B)% }}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod% _{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}% }{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}\Bigl{(}{\mathsf{fib}}_{f}(b)% \to\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{}\Bigr{)}.$

Since each map ${\mathsf{fib}}_{f}(b)\to\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}% \mathclose{}$ is $n$-connected by Corollary 7.5.8 (http://planetmath.org/75connectedness#Thmprecor2), $\tilde{f}$ is $n$-connected by Lemma 7.5.13 (http://planetmath.org/75connectedness#Thmprelem8). Finally, the projection $\mathsf{pr}_{1}:\mathsf{im}_{n}(f)\to B$ is $n$-truncated, since its fibers are equivalent to the $n$-truncations of the fibers of $f$. β

In the following lemma we set up some machinery to prove the unique factorization theorem.

###### Lemma 7.6.5.

Suppose we have a commutative diagram of functions

\includegraphics

HoTT_fig_7.6.1.png

with $H:h_{1}\circ g_{1}\sim h_{2}\circ g_{2}$, where $g_{1}$ and $g_{2}$ are $n$-connected and where $h_{1}$ and $h_{2}$ are $n$-truncated. Then there is an equivalence

 $E(H,b):{\mathsf{fib}}_{h_{1}}(b)\simeq{\mathsf{fib}}_{h_{2}}(b)$

for any $b:B$, such that for any $a:A$ we have an identification

 $\overline{E}(H,a):E(H,h_{1}(g_{1}(a)))({g_{1}(a),\mathsf{refl}_{h_{1}(g_{1}(a)% )}})={\mathopen{}(g_{2}(a),\mathord{{H(a)}^{-1}})\mathclose{}}.$
###### Proof.

Let $b:B$. Then we have the following equivalences:

 $\displaystyle{\mathsf{fib}}_{h_{1}}(b)$ $\displaystyle\simeq\mathchoice{\sum_{w:{\mathsf{fib}}_{h_{1}}(b)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{% \mathsf{fib}}_{h_{1}}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{h% _{1}}(b))}}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_% {1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\mathchoice{{\textstyle\sum_% {(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{% (w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}% \mathopen{}\left\|{\mathsf{fib}}_{g_{1}}(\mathsf{pr}_{1}w)\right\|_{n}% \mathclose{}{}$ (since $g_{1}$ is $n$-connected) $\displaystyle\simeq\Bigl{\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{h_{1}}(b)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{% \mathsf{fib}}_{h_{1}}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{h% _{1}}(b))}}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_% {1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\mathchoice{{\textstyle\sum_% {(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{% (w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\mathsf% {fib}}_{g_{1}}(\mathsf{pr}_{1}w)\Bigr{\|}_{n}{}$ (by Corollary 7.3.10 (http://planetmath.org/73truncationshmprecor2), since $h_{1}$ is $n$-truncated) $\displaystyle\simeq\mathopen{}\left\|{\mathsf{fib}}_{h_{1}\circ g_{1}}(b)% \right\|_{n}\mathclose{}{}$ (by http://planetmath.org/node/87774Exercise 4.4)

and likewise for $h_{2}$ and $g_{2}$. Also, since we have a homotopy $H:h_{1}\circ g_{1}\sim h_{2}\circ g_{2}$, there is an obvious equivalence ${\mathsf{fib}}_{h_{1}\circ g_{1}}(b)\simeq{\mathsf{fib}}_{h_{2}\circ g_{2}}(b)$. Hence we obtain

 ${\mathsf{fib}}_{h_{1}}(b)\simeq{\mathsf{fib}}_{h_{2}}(b)$

for any $b:B$. By analyzing the underlying functions, we get the following representation of what happens to the element ${\mathopen{}(g_{1}(a),\mathsf{refl}_{h_{1}(g_{1}(a))})\mathclose{}}$ after applying each of the equivalences of which $E$ is composed. Some of the identifications are definitional, but others (marked with a $=$ below) are only propositional; putting them together we obtain $\overline{E}(H,a)$.

 $\displaystyle{\mathopen{}(g_{1}(a),\mathsf{refl}_{h_{1}(g_{1}(a))})\mathclose{}}$ $\displaystyle\overset{=}{\mapsto}{\mathopen{}\left({\mathopen{}(g_{1}(a),% \mathsf{refl}_{h_{1}(g_{1}(a))})\mathclose{}},\mathopen{}\left|{\mathopen{}(a,% \mathsf{refl}_{g_{1}(a)})\mathclose{}}\right|_{n}\mathclose{}\right)\mathclose% {}}$ $\displaystyle\mapsto\mathopen{}\left|{\mathopen{}({\mathopen{}(g_{1}(a),% \mathsf{refl}_{h_{1}(g_{1}(a))})\mathclose{}},{\mathopen{}(a,\mathsf{refl}_{g_% {1}(a)})\mathclose{}})\mathclose{}}\right|_{n}\mathclose{}$ $\displaystyle\mapsto\mathopen{}\left|{\mathopen{}(a,\mathsf{refl}_{h_{1}(g_{1}% (a))})\mathclose{}}\right|_{n}\mathclose{}$ $\displaystyle\overset{=}{\mapsto}\mathopen{}\left|{\mathopen{}(a,\mathord{{H(a% )}^{-1}})\mathclose{}}\right|_{n}\mathclose{}$ $\displaystyle\mapsto\mathopen{}\left|{\mathopen{}({\mathopen{}(g_{2}(a),% \mathord{{H(a)}^{-1}})\mathclose{}},{\mathopen{}(a,\mathsf{refl}_{g_{2}(a)})% \mathclose{}})\mathclose{}}\right|_{n}\mathclose{}$ $\displaystyle\mapsto{\mathopen{}\left({\mathopen{}(g_{2}(a),\mathord{{H(a)}^{-% 1}})\mathclose{}},\mathopen{}\left|{\mathopen{}(a,\mathsf{refl}_{g_{2}(a)})% \mathclose{}}\right|_{n}\mathclose{}\right)\mathclose{}}$ $\displaystyle\mapsto{\mathopen{}(g_{2}(a),\mathord{{H(a)}^{-1}})\mathclose{}}$

The first equality is because for general $b$, the map ${\mathsf{fib}}_{h_{1}}(b)\to\mathchoice{\sum_{w:{\mathsf{fib}}_{h_{1}}(b)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{% \mathsf{fib}}_{h_{1}}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{h% _{1}}(b))}}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_% {1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\mathchoice{{\textstyle\sum_% {(w:{\mathsf{fib}}_{h_{1}}(b))}}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{% (w:{\mathsf{fib}}_{h_{1}}(b))}}{\sum_{(w:{\mathsf{fib}}_{h_{1}}(b))}}}% \mathopen{}\left\|{\mathsf{fib}}_{g_{1}}(\mathsf{pr}_{1}w)\right\|_{n}% \mathclose{}$ inserts the center of contraction for $\mathopen{}\left\|{\mathsf{fib}}_{g_{1}}(\mathsf{pr}_{1}w)\right\|_{n}% \mathclose{}$ supplied by the assumption that $g_{1}$ is $n$-truncated; whereas in the case in question this type has the obvious inhabitant $\mathopen{}\left|{\mathopen{}(a,\mathsf{refl}_{g_{1}(a)})\mathclose{}}\right|_% {n}\mathclose{}$, which by contractibility must be equal to the center. The second propositional equality is because the equivalence ${\mathsf{fib}}_{h_{1}\circ g_{1}}(b)\simeq{\mathsf{fib}}_{h_{2}\circ g_{2}}(b)$ concatenates the second components with $\mathord{{H(a)}^{-1}}$, and we have $\mathord{{H(a)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}\mathsf{refl}=\mathord{{H(a)}^{-1}}$. The reader may check that the other equalities are definitional (assuming a reasonable solution to http://planetmath.org/node/87774Exercise 4.4). β

Combining Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2),Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3), we have the following unique factorization result:

###### Theorem 7.6.6.

For each $f:A\to B$, the space $\mathsf{fact}_{n}(f)$ defined by

 $\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_{(g:A\to X)}\,}{\mathchoice{{\textstyle\sum_{(% g:A\to X)}}}{\sum_{(g:A\to X)}}{\sum_{(g:A\to X)}}{\sum_{(g:A\to X)}}}{% \mathchoice{{\textstyle\sum_{(g:A\to X)}}}{\sum_{(g:A\to X)}}{\sum_{(g:A\to X)% }}{\sum_{(g:A\to X)}}}{\mathchoice{{\textstyle\sum_{(g:A\to X)}}}{\sum_{(g:A% \to X)}}{\sum_{(g:A\to X)}}{\sum_{(g:A\to X)}}}\mathchoice{\sum_{(h:X\to B)}\,% }{\mathchoice{{\textstyle\sum_{(h:X\to B)}}}{\sum_{(h:X\to B)}}{\sum_{(h:X\to B% )}}{\sum_{(h:X\to B)}}}{\mathchoice{{\textstyle\sum_{(h:X\to B)}}}{\sum_{(h:X% \to B)}}{\sum_{(h:X\to B)}}{\sum_{(h:X\to B)}}}{\mathchoice{{\textstyle\sum_{(% h:X\to B)}}}{\sum_{(h:X\to B)}}{\sum_{(h:X\to B)}}{\sum_{(h:X\to B)}}}(h\circ g% \sim f)\times\mathsf{conn}_{n}(g)\times\mathsf{trunc}_{n}(h).$

is contractible. Its center of contraction is the element

 ${\mathopen{}(\mathsf{im}_{n}(f),\tilde{f},\mathsf{pr}_{1},\theta,\varphi,\psi)% \mathclose{}}:\mathsf{fact}_{n}(f)$

arising from Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2), where $\theta:\mathsf{pr}_{1}\circ\tilde{f}\sim f$ is the canonical homotopy, where $\varphi$ is the proof of Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2), and where $\psi$ is the obvious proof that $\mathsf{pr}_{1}:\mathsf{im}_{n}(f)\to B$ has $n$-truncated fibers.

###### Proof.

By Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2) we know that there is an element of $\mathsf{fact}_{n}(f)$, hence it is enough to show that $\mathsf{fact}_{n}(f)$ is a mere proposition. Suppose we have two $n$-factorizations

 ${\mathopen{}(X_{1},g_{1},h_{1},H_{1},\varphi_{1},\psi_{1})\mathclose{}}\qquad% \text{and}\qquad{\mathopen{}(X_{2},g_{2},h_{2},H_{2},\varphi_{2},\psi_{2})% \mathclose{}}$

of $f$. Then we have the pointwise-concatenated homotopy

 $H:\!\!\equiv({\lambda}a.\,H_{1}(a)\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}H_{2}^{-1}(a))\,:\,(h_{1}\circ g% _{1}\sim h_{2}\circ g_{2}).$

By univalence and the characterization of paths and transport in $\Sigma$-types, function types, and path types, it suffices to show that

1. 1.

there is an equivalence $e:X_{1}\simeq X_{2}$,

2. 2.

there is a homotopy $\zeta:e\circ g_{1}\sim g_{2}$,

3. 3.

there is a homotopy $\eta:h_{2}\circ e\sim h_{1}$,

4. 4.

for any $a:A$ we have $\mathord{{\mathsf{ap}_{h_{2}}(\zeta(a))}^{-1}}\mathchoice{\mathbin{\raisebox{2% .15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}% {\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\eta(g_{1}(a))% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}H_{1}(a)=H_{2}(a)$.

We prove these four assertions in that order.

1. 1.

By Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3), we have a fiberwise equivalence

 $E(H):\mathchoice{\prod_{b:B}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{% (b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathsf{fib}}_{h_{1}}(b)% \simeq{\mathsf{fib}}_{h_{2}}(b).$

This induces an equivalence of total spaces, i.e.Β we have

 $\Bigl{(}\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}}_{h_{1}}(b)\Bigr{)}% \;\simeq\;\Bigl{(}\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}}_{h_{2}}(b)% \Bigr{)}.$

Of course, we also have the equivalences $X_{1}\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}}_{h_{1}}(b)$ and $X_{2}\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}}_{h_{2}}(b)$ from Lemma 4.8.2 (http://planetmath.org/48theobjectclassifier#Thmprelem2). This gives us our equivalence $e:X_{1}\simeq X_{2}$; the reader may verify that the underlying function of $e$ is given by

 $e(x)\equiv\mathsf{pr}_{1}(E(H,h_{1}(x))(x,\mathsf{refl}_{h_{1}(x)})).$
2. 2.

By Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3), we may choose $\zeta(a):\!\!\equiv\mathsf{ap}_{\mathsf{pr}_{1}}(\overline{E}(H,a)):e(g_{1}(a)% )=g_{2}(a)$.

3. 3.

For every $x:X_{1}$, we have

 $\mathsf{pr}_{2}(E(H,h_{1}(x))({x,\mathsf{refl}_{h_{1}(x)}})):h_{2}(e(x))=h_{1}% (x),$

giving us a homotopy $\eta:h_{2}\circ e\sim h_{1}$.

4. 4.

By the characterization of paths in fibers (Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2)), the path $\overline{E}(H,a)$ from Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3) gives us $\eta(g_{1}(a))=\mathsf{ap}_{h_{2}}(\zeta(a))\mathchoice{\mathbin{\raisebox{2.1% 5pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{H(a)}^{-1}}$. The desired equality follows by substituting the definition of $H$ and rearranging paths.β

By standard arguments, this yields the following orthogonality principle.

###### Theorem 7.6.7.

Let $e:A\to B$ be $n$-connected and $m:C\to D$ be $n$-truncated. Then the map

 $\varphi:(B\to C)\;\to\;\mathchoice{\sum_{(h:A\to C)}\,}{\mathchoice{{% \textstyle\sum_{(h:A\to C)}}}{\sum_{(h:A\to C)}}{\sum_{(h:A\to C)}}{\sum_{(h:A% \to C)}}}{\mathchoice{{\textstyle\sum_{(h:A\to C)}}}{\sum_{(h:A\to C)}}{\sum_{% (h:A\to C)}}{\sum_{(h:A\to C)}}}{\mathchoice{{\textstyle\sum_{(h:A\to C)}}}{% \sum_{(h:A\to C)}}{\sum_{(h:A\to C)}}{\sum_{(h:A\to C)}}}\mathchoice{\sum_{(k:% B\to D)}\,}{\mathchoice{{\textstyle\sum_{(k:B\to D)}}}{\sum_{(k:B\to D)}}{\sum% _{(k:B\to D)}}{\sum_{(k:B\to D)}}}{\mathchoice{{\textstyle\sum_{(k:B\to D)}}}{% \sum_{(k:B\to D)}}{\sum_{(k:B\to D)}}{\sum_{(k:B\to D)}}}{\mathchoice{{% \textstyle\sum_{(k:B\to D)}}}{\sum_{(k:B\to D)}}{\sum_{(k:B\to D)}}{\sum_{(k:B% \to D)}}}(m\circ h\sim k\circ e)$

is an equivalence.

###### Sketch of proof.

For any $(h,k,H)$ in the codomain, let $h=h_{2}\circ h_{1}$ and $k=k_{2}\circ k_{1}$, where $h_{1}$ and $k_{1}$ are $n$-connected and $h_{2}$ and $k_{2}$ are $n$-truncated. Then $f=(m\circ h_{2})\circ h_{1}$ and $f=k_{2}\circ(k_{1}\circ e)$ are both $n$-factorizations of $m\circ h=k\circ e$. Thus, there is a unique equivalence between them. It is straightforward (if a bit tedious) to extract from this that ${\mathsf{fib}}_{\varphi}((h,k,H))$ is contractible. β

We end by showing that images are stable under pullback.

###### Lemma 7.6.8.

Suppose that the square

\includegraphics

HoTT_fig_7.6.2.png

is a pullback square and let $b:B$. Then ${\mathsf{fib}}_{f}(b)\simeq{\mathsf{fib}}_{g}(h(b))$.

###### Proof.

This follows from pasting of pullbacks (http://planetmath.org/node/87643Exercise 2.12), since the type $X$ in the diagram

\includegraphics

HoTT_fig_7.6.3.png

is the pullback of the left square if and only if it is the pullback of the outer rectangle, while ${\mathsf{fib}}_{f}(b)$ is the pullback of the square on the left and ${\mathsf{fib}}_{g}(h(b))$ is the pullback of the outer rectangle. β

###### Theorem 7.6.9.

Consider functions $f:A\to B$, $g:C\to D$ and the diagram

\includegraphics

HoTT_fig_7.6.4.png

If the outer rectangle is a pullback, then so is the bottom square (and hence so is the top square, by http://planetmath.org/node/87643Exercise 2.12). Consequently, images are stable under pullbacks.

###### Proof.

Assuming the outer square is a pullback, we have equivalences

 $\displaystyle B\times_{D}\mathsf{im}_{n}(g)$ $\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_{(w:% \mathsf{im}_{n}(g))}\,}{\mathchoice{{\textstyle\sum_{(w:\mathsf{im}_{n}(g))}}}% {\sum_{(w:\mathsf{im}_{n}(g))}}{\sum_{(w:\mathsf{im}_{n}(g))}}{\sum_{(w:% \mathsf{im}_{n}(g))}}}{\mathchoice{{\textstyle\sum_{(w:\mathsf{im}_{n}(g))}}}{% \sum_{(w:\mathsf{im}_{n}(g))}}{\sum_{(w:\mathsf{im}_{n}(g))}}{\sum_{(w:\mathsf% {im}_{n}(g))}}}{\mathchoice{{\textstyle\sum_{(w:\mathsf{im}_{n}(g))}}}{\sum_{(% w:\mathsf{im}_{n}(g))}}{\sum_{(w:\mathsf{im}_{n}(g))}}{\sum_{(w:\mathsf{im}_{n% }(g))}}}h(b)=\mathsf{pr}_{1}w$ $\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_{(d:% D)}\,}{\mathchoice{{\textstyle\sum_{(d:D)}}}{\sum_{(d:D)}}{\sum_{(d:D)}}{\sum_% {(d:D)}}}{\mathchoice{{\textstyle\sum_{(d:D)}}}{\sum_{(d:D)}}{\sum_{(d:D)}}{% \sum_{(d:D)}}}{\mathchoice{{\textstyle\sum_{(d:D)}}}{\sum_{(d:D)}}{\sum_{(d:D)% }}{\sum_{(d:D)}}}\mathchoice{\sum_{(w:\mathopen{}\left\|{\mathsf{fib}}_{g}(d)% \right\|_{n}\mathclose{})}\,}{\mathchoice{{\textstyle\sum_{(w:\mathopen{}\left% \|{\mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}}{\sum_{(w:\mathopen{}\left% \|{\mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}{\sum_{(w:\mathopen{}\left\|% {\mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}{\sum_{(w:\mathopen{}\left\|{% \mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}}{\mathchoice{{\textstyle\sum_{% (w:\mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}}{\sum_{(% w:\mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}{\sum_{(w:% \mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}{\sum_{(w:% \mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right\|_{n}\mathclose{})}}}{% \mathchoice{{\textstyle\sum_{(w:\mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right% \|_{n}\mathclose{})}}}{\sum_{(w:\mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right% \|_{n}\mathclose{})}}{\sum_{(w:\mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right\|% _{n}\mathclose{})}}{\sum_{(w:\mathopen{}\left\|{\mathsf{fib}}_{g}(d)\right\|_{% n}\mathclose{})}}}h(b)=d$ $\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)}}}\mathopen{}\left\|{% \mathsf{fib}}_{g}(h(b))\right\|_{n}\mathclose{}$ $\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)}}}\mathopen{}\left\|{% \mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{}$ (by Theorem 7.6.9 (http://planetmath.org/76orthogonalfactorization#Thmprethm3)) $\displaystyle\equiv\mathsf{im}_{n}(f).$ $\displaystyle\qed$
Title 7.6 Orthogonal factorization
\metatable