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.

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

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

there is a homotopy $\eta:h_{2}\circ e\sim h_{1}$ ,
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.

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.

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)$ .

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.

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

	$\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{}}$