7.5 Connectedness

An $n$ -type is one that has no interesting information above dimension $n$ . By contrast, an $n$ -connected type is one that has no interesting information below dimension $n$ . It turns out to be natural to study a more general notion for functions as well.

Definition 7.5.1.

A function $f:A\to B$ is said to be $n$ -connected if for all $b : B$ , the type $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{}$ is contractible:

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

A type $A$ is said to be $n$ -connected if the unique function $A\to\mathbf{1}$ is $n$ -connected, i.e. if $\mathopen{}\left\|A\right\|_{n}\mathclose{}$ is contractible.

Thus, a function $f:A\to B$ is $n$ -connected if and only if ${\mathsf{fib}}_{f}(b)$ is $n$ -connected for every $b : B$ . Of course, every function is $(-2)$ -connected. At the next level, we have:

Lemma 7.5.2.

A function $f$ is $(-1)$ -connected if and only if it is surjective in the sense of §4.6 (http://planetmath.org/46surjectionsandembeddings).

Proof.

We defined $f$ to be surjective if $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{-1}\mathclose{}$ is inhabited for all $b$ . But since it is a mere proposition, inhabitation is equivalent to contractibility. ∎

Thus, $n$ -connectedness of a function for $n\geq 0$ can be thought of as a strong form of surjectivity. Category-theoretically, $(-1)$ -connectedness corresponds to essential surjectivity on objects, while $n$ -connectedness corresponds to essential surjectivity on $k$ -morphisms for $k\leq n+1$ .

Lemma 7.5.2 (http://planetmath.org/75connectedness#Thmprelem1) also implies that a type $A$ is $(-1)$ -connected if and only if it is merely inhabited. When a type is $0$ -connected we may simply say that it is connected, and when it is $1$ -connected we say it is simply connected.

Remark 7.5.3.

While our notion of $n$ -connectedness for types agrees with the standard notion in homotopy theory, our notion of $n$ -connectedness for functions is off by one from a common indexing in classical homotopy theory. Whereas we say a function $f$ is $n$ -connected if all its fibers are $n$ -connected, some classical homotopy theorists would call such a function $(n+1)$ -connected. (This is due to a historical focus on cofibers rather than fibers.)

We now observe a few closure properties of connected maps.

Lemma 7.5.4.

Suppose that $g$ is a retract of a $n$ -connected function $f$ . Then $g$ is $n$ -connected.

Proof.

This is a direct consequence of Lemma 4.7.3 (http://planetmath.org/47closurepropertiesofequivalences#Thmprelem1). ∎

Corollary 7.5.5.

If $g$ is homotopic to a $n$ -connected function $f$ , then $g$ is $n$ -connected.

Lemma 7.5.6.

Suppose that $f:A\to B$ is $n$ -connected. Then $g:B\to C$ is $n$ -connected if and only if $g\circ f$ is $n$ -connected.

Proof.

For any $c : C$ , we have

$\displaystyle\mathopen{}\left\\|{\mathsf{fib}}_{g\circ f}(c)\right\\|_{n}% \mathclose{}$	$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{g}(c)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(% c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{% \sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}}{\mathsf{fib}}_{f}(\mathsf{pr}_{1}w)\Bigr{\\|}_{n}{}$	(by http://planetmath.org/node/87774Exercise 4.4)
	$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{g}(c)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(% c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{% \sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}}\mathopen{}\left\\|{\mathsf{fib}}_{f}(\mathsf{pr}_{1}w)% \right\\|_{n}\mathclose{}\Bigr{\\|}_{n}{}$	(by Theorem 7.3.9 (http://planetmath.org/73truncationshmprethm3))
	$\displaystyle\simeq\mathopen{}\left\\|{\mathsf{fib}}_{g}(c)\right\\|_{n}% \mathclose{}.{}$	(since $\mathopen{}\left\\|{\mathsf{fib}}_{f}(\mathsf{pr}_{1}w)\right\\|_{n}\mathclose{}$ is contractible)

It follows that $\mathopen{}\left\|{\mathsf{fib}}_{g}(c)\right\|_{n}\mathclose{}$ is contractible if and only if $\mathopen{}\left\|{\mathsf{fib}}_{g\circ f}(c)\right\|_{n}\mathclose{}$ is contractible. ∎

Importantly, $n$ -connected functions can be equivalently characterized as those which satisfy an “induction principle” with respect to $n$ -types. This idea will lead directly into our proof of the Freudenthal suspension theorem in §8.6 (http://planetmath.org/86thefreudenthalsuspensiontheorem).

Lemma 7.5.7.

For $f:A\to B$ and $P:B\to\mathcal{U}$ , consider the following function:

{\lambda}s.\,s\circ f:\Bigl{(}\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)}}}P(b)\Bigr{)}\to\Bigl{(}\mathchoice{\prod_{a:A}\,}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{% \mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a% :A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{% \prod_{(a:A)}}}P(f(a))\Bigr{)}.

For a fixed $f$ and $n\geq-2$ , the following are equivalent.

1.

$f$ is $n$ -connected.
2.

For every $P:B\to{n}\text{-}\mathsf{Type}$ , the map ${\lambda}s.\,s\circ f$ is an equivalence.
3.

For every $P:B\to{n}\text{-}\mathsf{Type}$ , the map ${\lambda}s.\,s\circ f$ has a section.

Proof.

Suppose that $f$ is $n$ -connected and let $P:B\to{n}\text{-}\mathsf{Type}$ . Then we have the equivalences

$\displaystyle\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)}}}P(b)$	$\displaystyle\simeq\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{(% }\mathopen{}\left\\|{\mathsf{fib}}_{f}(b)\right\\|_{n}\mathclose{}\to P(b)\Bigr{% )}{}$	(since $\mathopen{}\left\\|{\mathsf{fib}}_{f}(b)\right\\|_{n}\mathclose{}$ is contractible)
	$\displaystyle\simeq\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 P(b)\Bigr{)}{}$	(since $P(b)$ is an $n$-type)
	$\displaystyle\simeq\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)}}}% \mathchoice{\prod_{(a:A)}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(p:f(a)% =b)}\,}{\mathchoice{{\textstyle\prod_{(p:f(a)=b)}}}{\prod_{(p:f(a)=b)}}{\prod_% {(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}}{\mathchoice{{\textstyle\prod_{(p:f(a)=b)}}}% {\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}}{\mathchoice{{% \textstyle\prod_{(p:f(a)=b)}}}{\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}{\prod_{% (p:f(a)=b)}}}P(b){}$	(by the left universal property of $\Sigma$-types)
	$\displaystyle\simeq\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle% \prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{% \textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}P(f(a))% .{}$	(by the left universal property of path types)

We omit the proof that this equivalence is indeed given by ${\lambda}s.\,s\circ f$ . Thus, 1 $\Rightarrow$ 2, and clearly 2 $\Rightarrow$ 3. To show 3 $\Rightarrow$ 1, consider the type family

P(b):\!\!\equiv\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{}.

Then 3 yields a map $c:\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)}}}\mathopen{}\left\|{\mathsf% {fib}}_{f}(b)\right\|_{n}\mathclose{}$ with $c(f(a))=\mathopen{}\left|{\mathopen{}(a,\mathsf{refl}_{f(a)})\mathclose{}}% \right|_{n}\mathclose{}$ . To show that each $\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{}$ is contractible, we will find a function of type

\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)}}}\mathchoice{\prod_{(w:% \mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}\,}{% \mathchoice{{\textstyle\prod_{(w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right% \|_{n}\mathclose{})}}}{\prod_{(w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right% \|_{n}\mathclose{})}}{\prod_{(w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right% \|_{n}\mathclose{})}}{\prod_{(w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right% \|_{n}\mathclose{})}}}{\mathchoice{{\textstyle\prod_{(w:\mathopen{}\left\|{% \mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}}{\prod_{(w:\mathopen{}\left\|{% \mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}{\prod_{(w:\mathopen{}\left\|{% \mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}{\prod_{(w:\mathopen{}\left\|{% \mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}}{\mathchoice{{\textstyle\prod_% {(w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}}{\prod_% {(w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}{\prod_{% (w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}{\prod_{(% w:\mathopen{}\left\|{\mathsf{fib}}_{f}(b)\right\|_{n}\mathclose{})}}}w=c(b).

By Theorem 7.3.2 (http://planetmath.org/73truncations#Thmprethm1), for this it suffices to find a function of type

\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)}}}\mathchoice{\prod_{(a:A)}% \,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod% _{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}% }{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_% {(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(p:f(a)=b)}\,}{\mathchoice{{% \textstyle\prod_{(p:f(a)=b)}}}{\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}{\prod_{% (p:f(a)=b)}}}{\mathchoice{{\textstyle\prod_{(p:f(a)=b)}}}{\prod_{(p:f(a)=b)}}{% \prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}}{\mathchoice{{\textstyle\prod_{(p:f(a)% =b)}}}{\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}{\prod_{(p:f(a)=b)}}}\mathopen{}% \left|{\mathopen{}(a,p)\mathclose{}}\right|_{n}\mathclose{}=c(b).

But by rearranging variables and path induction, this is equivalent to the type

\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\mathopen{}\left|{\mathopen{}(a% ,\mathsf{refl}_{f(a)})\mathclose{}}\right|_{n}\mathclose{}=c(f(a)).

This property holds by our choice of $c(f(a))$ . ∎

Corollary 7.5.8.

For any $A$ , the canonical function $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}:A\to\mathopen{}\left\|A% \right\|_{n}\mathclose{}$ is $n$ -connected.

Proof.

By Theorem 7.3.2 (http://planetmath.org/73truncations#Thmprethm1) and the associated uniqueness principle, the condition of Lemma 7.5.7 (http://planetmath.org/75connectedness#Thmprelem4) holds. ∎

For instance, when $n=-1$ , Corollary 7.5.8 (http://planetmath.org/75connectedness#Thmprecor2) says that the map $A\to\mathopen{}\left\|A\right\|\mathclose{}$ from a type to its propositional truncation is surjective.

Corollary 7.5.9.

A type $A$ is $n$ -connected if and only if the map

{\lambda}b.\,{\lambda}a.\,b:B\to(A\to B)

is an equivalence for every $n$ -type $B$ . In other words, “every map from $A$ to an $n$ -type is constant”.

Proof.

By Lemma 7.5.7 (http://planetmath.org/75connectedness#Thmprelem4) applied to a function with codomain $\mathbf{1}$ . ∎

Lemma 7.5.10.

Let $B$ be an $n$ -type and let $f:A\to B$ be a function. Then the induced function $g:\mathopen{}\left\|A\right\|_{n}\mathclose{}\to B$ is an equivalence if and only if $f$ is $n$ -connected.

Proof.

By Corollary 7.5.8 (http://planetmath.org/75connectedness#Thmprecor2), $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}$ is $n$ -connected. Thus, since $f=g\circ|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}$ , by Lemma 7.5.6 (http://planetmath.org/75connectedness#Thmprelem3) $f$ is $n$ -connected if and only if $g$ is $n$ -connected. But since $g$ is a function between $n$ -types, its fibers are also $n$ -types. Thus, $g$ is $n$ -connected if and only if it is an equivalence. ∎

We can also characterize connected pointed types in terms of connectivity of the inclusion of their basepoint.

Lemma 7.5.11.

Let $A$ be a type and $a_{0}:\mathbf{1}\to A$ a basepoint, with $n\geq-1$ . Then $A$ is $n$ -connected if and only if the map $a_{0}$ is $(n-1)$ -connected.

Proof.

First suppose $a_{0}:\mathbf{1}\to A$ is $(n-1)$ -connected and let $B$ be an $n$ -type; we will use Corollary 7.5.9 (http://planetmath.org/75connectedness#Thmprecor3). The map ${\lambda}b.\,{\lambda}a.\,b:B\to(A\to B)$ has a retraction given by $f\mapsto f(a_{0})$ , so it suffices to show it also has a section, i.e. that for any $f:A\to B$ there is $b : B$ such that $f={\lambda}a.\,b$ . We choose $b:\!\!\equiv f(a_{0})$ . Define $P:A\to\mathcal{U}$ by $P(a):\!\!\equiv(f(a)=f(a_{0}))$ . Then $P$ is a family of $(n-1)$ -types and we have $P(a_{0})$ ; hence we have $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}P(a)$ since $a_{0}:\mathbf{1}\to A$ is $(n-1)$ -connected. Thus, $f={\lambda}a.\,f(a_{0})$ as desired.

Now suppose $A$ is $n$ -connected, and let $P:A\to{(n-1)}\text{-}\mathsf{Type}$ and $u:P(a_{0})$ be given. By Lemma 7.5.7 (http://planetmath.org/75connectedness#Thmprelem4), it will suffice to construct $f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}P(a)$ such that $f(a_{0})=u$ . Now ${(n-1)}\text{-}\mathsf{Type}$ is an $n$ -type and $A$ is $n$ -connected, so by Corollary 7.5.9 (http://planetmath.org/75connectedness#Thmprecor3), there is an $n$ -type $B$ such that $P={\lambda}a.\,B$ . Hence, we have a family of equivalences $g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}(P(a)\simeq B)$ . Define $f(a):\!\!\equiv\mathord{{g_{a}}^{-1}}(g_{a_{0}}(u))$ ; then $f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}P(a)$ and $f(a_{0})=u$ as desired. ∎

In particular, a pointed type $(A,a_{0})$ is 0-connected if and only if $a_{0}:\mathbf{1}\to A$ is surjective, which is to say $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}\mathopen{}\left\|x=a_{0}\right% \|\mathclose{}$ .

A useful variation on Lemma 7.5.6 (http://planetmath.org/75connectedness#Thmprelem3) is:

Lemma 7.5.12.

Let $f:A\to B$ be a function and $P:A\to\mathcal{U}$ and $Q:B\to\mathcal{U}$ be type families. Suppose that $g:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}P(a)\to Q(f(a))$ is a fiberwise $n$ -connected family of functions, i.e. each function $g_{a}:P(a)\to Q(f(a))$ is $n$ -connected. Then the function

	$\displaystyle\varphi$	$\displaystyle:\Bigl{(}\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)}}}P(a)\Bigr{)}\to\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)}}}Q(b)\Bigr{)}$
	$\displaystyle\varphi(a,u)$	$\displaystyle:\!\!\equiv{\mathopen{}(f(a),g_{a}(u))\mathclose{}}$

is $n$ -connected if and only if $f$ is $n$ -connected.

Proof.

For $b : B$ and $v:Q(b)$ we have

	$\displaystyle\mathopen{}\left\\|{\mathsf{fib}}_{\varphi}({\mathopen{}(b,v)% \mathclose{}})\right\\|_{n}\mathclose{}$	$\displaystyle\simeq\Bigl{\\|}\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_{(u:P(a))}\,}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{% \sum_{(u:P(a))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{\mathchoice{{\textstyle% \sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{% \mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}{% \sum_{(u:P(a))}}}\mathchoice{\sum_{(p:f(a)=b)}\,}{\mathchoice{{\textstyle\sum_% {(p:f(a)=b)}}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)}}}{% \mathchoice{{\textstyle\sum_{(p:f(a)=b)}}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)% }}{\sum_{(p:f(a)=b)}}}{\mathchoice{{\textstyle\sum_{(p:f(a)=b)}}}{\sum_{(p:f(a% )=b)}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)}}}{{f}\mathopen{}\left({p}\right)% \mathclose{}}_{*}\mathopen{}\left({g_{a}(u)}\right)\mathclose{}=v\Bigr{\\|}_{n}$
		$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{(w:{\mathsf{fib}}_{f}(b))}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(% b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{% \sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}}\mathchoice{\sum_{(u:P(\mathsf{pr}_{1}(w)))}\,}{% \mathchoice{{\textstyle\sum_{(u:P(\mathsf{pr}_{1}(w)))}}}{\sum_{(u:P(\mathsf{% pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)% ))}}}{\mathchoice{{\textstyle\sum_{(u:P(\mathsf{pr}_{1}(w)))}}}{\sum_{(u:P(% \mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr% }_{1}(w)))}}}{\mathchoice{{\textstyle\sum_{(u:P(\mathsf{pr}_{1}(w)))}}}{\sum_{% (u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(% \mathsf{pr}_{1}(w)))}}}g_{\mathsf{pr}_{1}w}(u)={\mathord{{{f}\mathopen{}\left(% {\mathsf{pr}_{2}w}\right)\mathclose{}}^{-1}}}_{*}\mathopen{}\left({v}\right)% \mathclose{}\Bigr{\\|}_{n}$
		$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{f}(b)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(% b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{% \sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}}{\mathsf{fib}}_{g(\mathsf{pr}_{1}w)}({\mathord{{{f}% \mathopen{}\left({\mathsf{pr}_{2}w}\right)\mathclose{}}^{-1}}}_{*}\mathopen{}% \left({v}\right)\mathclose{})\Bigr{\\|}_{n}$
		$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{f}(b)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(% b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{% \sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}}\mathopen{}\left\\|{\mathsf{fib}}_{g(\mathsf{pr}_{1}w)}% ({\mathord{{{f}\mathopen{}\left({\mathsf{pr}_{2}w}\right)\mathclose{}}^{-1}}}_% {*}\mathopen{}\left({v}\right)\mathclose{})\right\\|_{n}\mathclose{}\Bigr{\\|}_{n}$
		$\displaystyle\simeq\mathopen{}\left\\|{\mathsf{fib}}_{f}(b)\right\\|_{n}% \mathclose{}$

where the transportations along $f(p)$ and $f(p)^{-1}$ are with respect to $Q$ . Therefore, if either is contractible, so is the other. ∎

In the other direction, we have

Lemma 7.5.13.

Let $P,Q:A\to\mathcal{U}$ be type families and consider a fiberwise transformation

f:\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:% A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{% \prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a% :A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\Bigl{(}P(a)\to Q(a)\Bigr{)}

from $P$ to $Q$ . Then the induced map $\mathsf{total}(f):\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)}}}P(a)\to\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)}}}Q(a)$ is $n$ -connected if and only if each $f(a)$ is $n$ -connected.

Proof.

By Theorem 4.7.6 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm3), we have ${\mathsf{fib}}_{\mathsf{total}(f)}({\mathopen{}(x,v)\mathclose{}})\simeq{% \mathsf{fib}}_{f(x)}(v)$ for each $x : A$ and $v:Q(x)$ . Hence $\mathopen{}\left\|{\mathsf{fib}}_{\mathsf{total}(f)}({\mathopen{}(x,v)% \mathclose{}})\right\|_{n}\mathclose{}$ is contractible if and only if $\mathopen{}\left\|{\mathsf{fib}}_{f(x)}(v)\right\|_{n}\mathclose{}$ is contractible. ∎

Another useful fact about connected maps is that they induce an equivalence on $n$ -truncations:

Lemma 7.5.14.

If $f:A\to B$ is $n$ -connected, then it induces an equivalence $\mathopen{}\left\|A\right\|_{n}\mathclose{}\simeq\mathopen{}\left\|B\right\|_{% n}\mathclose{}$ .

Proof.

Let $c$ be the proof that $f$ is $n$ -connected. From left to right, we use the map $\mathopen{}\left\|f\right\|_{n}\mathclose{}:\mathopen{}\left\|A\right\|_{n}% \mathclose{}\to\mathopen{}\left\|B\right\|_{n}\mathclose{}$ . To define the map from right to left, by the universal property of truncations, it suffices to give a map $\mathsf{back}:B\to{\mathopen{}\left\|A\right\|_{n}\mathclose{}}$ . We can define this map as follows:

\mathsf{back}(y):\!\!\equiv\mathopen{}\left\|\mathsf{pr}_{1}\right\|_{n}% \mathclose{}{(\mathsf{pr}_{1}{(c(y))})}

By definition, $c(y)$ has type $\mathsf{isContr}(\mathopen{}\left\|{\mathsf{fib}}_{f}(y)\right\|_{n}\mathclose% {})$ , so its first component has type $\mathopen{}\left\|{\mathsf{fib}}_{f}(y)\right\|_{n}\mathclose{}$ , and we can obtain an element of $\mathopen{}\left\|A\right\|_{n}\mathclose{}$ from this by projection.

Next, we show that the composites are the identity. In both directions, because the goal is a path in an $n$ -truncated type, it suffices to cover the case of the constructor $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}$ .

In one direction, we must show that for all $x : A$ ,

\mathopen{}\left\|\mathsf{pr}_{1}\right\|_{n}\mathclose{}{(\mathsf{pr}_{1}{(c(% f(x)))})}=\mathopen{}\left|x\right|_{n}\mathclose{}

But $\mathopen{}\left|(x,\mathsf{refl})\right|_{n}\mathclose{}:\mathopen{}\left\|{% \mathsf{fib}}_{f}(y)\right\|_{n}\mathclose{}$ , and $c(y)$ says that this type is contractible, so

\mathsf{pr}_{1}{(c(f(x)))}=\mathopen{}\left|(x,\mathsf{refl})\right|_{n}% \mathclose{}

Applying $\mathopen{}\left\|\mathsf{pr}_{1}\right\|_{n}\mathclose{}$ to both sides of this equation gives the result.

In the other direction, we must show that for all $y : B$ ,

\mathopen{}\left\|f\right\|_{n}\mathclose{}(\mathopen{}\left\|\mathsf{pr}_{1}% \right\|_{n}\mathclose{}(\mathsf{pr}_{1}{(c(y))}))=\mathopen{}\left|y\right|_{% n}\mathclose{}

$\mathsf{pr}_{1}{(c(y))}$ has type $\mathopen{}\left\|{\mathsf{fib}}_{f}(y)\right\|_{n}\mathclose{}$ , and the path we want is essentially the second component of the ${\mathsf{fib}}_{f}(y)$ , but we need to make sure the truncations work out.

In general, suppose we are given $p:\mathopen{}\left\|\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)\right\|_{n}% \mathclose{}$ and wish to prove $P(\mathopen{}\left\|\mathsf{pr}_{1}{}\right\|_{n}\mathclose{}(p))$ . By truncation induction, it suffices to prove $P(\mathopen{}\left|a\right|_{n}\mathclose{})$ for all $a : A$ and $b:B(a)$ . Applying this principle in this case, it suffices to prove

\mathopen{}\left\|f\right\|_{n}\mathclose{}(\mathopen{}\left|a\right|_{n}% \mathclose{})=\mathopen{}\left|y\right|_{n}\mathclose{}

given $a : A$ and $b:f(a)=y$ . But the left-hand side equals $\mathopen{}\left|f(a)\right|_{n}\mathclose{}$ , so applying $|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}|_{n}$ to both sides of $b$ gives the result. ∎

One might guess that this fact characterizes the $n$ -connected maps, but in fact being $n$ -connected is a bit stronger than this. For instance, the inclusion ${0_{\mathbf{2}}}:\mathbf{1}\to\mathbf{2}$ induces an equivalence on $(-1)$ -truncations, but is not surjective (i.e. $(-1)$ -connected). In §8.4 (http://planetmath.org/84fibersequencesandthelongexactsequence) we will see that the difference in general is an analogous extra bit of surjectivity.

Title	7.5 Connectedness
\metatable

$\displaystyle\mathopen{}\left\\|{\mathsf{fib}}_{g\circ f}(c)\right\\|_{n}% \mathclose{}$	$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{g}(c)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(% c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{% \sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}}{\mathsf{fib}}_{f}(\mathsf{pr}_{1}w)\Bigr{\\|}_{n}{}$	(by http://planetmath.org/node/87774Exercise 4.4)
	$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{g}(c)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(% c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{% fib}}_{g}(c))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{g}(c))}}}{% \sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{\mathsf{fib}}_{g}(c))}}{\sum_{(w:{% \mathsf{fib}}_{g}(c))}}}\mathopen{}\left\\|{\mathsf{fib}}_{f}(\mathsf{pr}_{1}w)% \right\\|_{n}\mathclose{}\Bigr{\\|}_{n}{}$	(by Theorem 7.3.9 (http://planetmath.org/73truncationshmprethm3))
	$\displaystyle\simeq\mathopen{}\left\\|{\mathsf{fib}}_{g}(c)\right\\|_{n}% \mathclose{}.{}$	(since $\mathopen{}\left\\|{\mathsf{fib}}_{f}(\mathsf{pr}_{1}w)\right\\|_{n}\mathclose{}$ is contractible)

	$\displaystyle\mathopen{}\left\\|{\mathsf{fib}}_{\varphi}({\mathopen{}(b,v)% \mathclose{}})\right\\|_{n}\mathclose{}$	$\displaystyle\simeq\Bigl{\\|}\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_{(u:P(a))}\,}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{% \sum_{(u:P(a))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{\mathchoice{{\textstyle% \sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{% \mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}{% \sum_{(u:P(a))}}}\mathchoice{\sum_{(p:f(a)=b)}\,}{\mathchoice{{\textstyle\sum_% {(p:f(a)=b)}}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)}}}{% \mathchoice{{\textstyle\sum_{(p:f(a)=b)}}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)% }}{\sum_{(p:f(a)=b)}}}{\mathchoice{{\textstyle\sum_{(p:f(a)=b)}}}{\sum_{(p:f(a% )=b)}}{\sum_{(p:f(a)=b)}}{\sum_{(p:f(a)=b)}}}{{f}\mathopen{}\left({p}\right)% \mathclose{}}_{*}\mathopen{}\left({g_{a}(u)}\right)\mathclose{}=v\Bigr{\\|}_{n}$
		$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{(w:{\mathsf{fib}}_{f}(b))}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(% b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{% \sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}}\mathchoice{\sum_{(u:P(\mathsf{pr}_{1}(w)))}\,}{% \mathchoice{{\textstyle\sum_{(u:P(\mathsf{pr}_{1}(w)))}}}{\sum_{(u:P(\mathsf{% pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)% ))}}}{\mathchoice{{\textstyle\sum_{(u:P(\mathsf{pr}_{1}(w)))}}}{\sum_{(u:P(% \mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr% }_{1}(w)))}}}{\mathchoice{{\textstyle\sum_{(u:P(\mathsf{pr}_{1}(w)))}}}{\sum_{% (u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(\mathsf{pr}_{1}(w)))}}{\sum_{(u:P(% \mathsf{pr}_{1}(w)))}}}g_{\mathsf{pr}_{1}w}(u)={\mathord{{{f}\mathopen{}\left(% {\mathsf{pr}_{2}w}\right)\mathclose{}}^{-1}}}_{*}\mathopen{}\left({v}\right)% \mathclose{}\Bigr{\\|}_{n}$
		$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{f}(b)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(% b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{% \sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}}{\mathsf{fib}}_{g(\mathsf{pr}_{1}w)}({\mathord{{{f}% \mathopen{}\left({\mathsf{pr}_{2}w}\right)\mathclose{}}^{-1}}}_{*}\mathopen{}% \left({v}\right)\mathclose{})\Bigr{\\|}_{n}$
		$\displaystyle\simeq\Bigl{\\|}\mathchoice{\sum_{w:{\mathsf{fib}}_{f}(b)}\,}{% \mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(% b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{% fib}}_{f}(b))}}}{\mathchoice{{\textstyle\sum_{(w:{\mathsf{fib}}_{f}(b))}}}{% \sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{\mathsf{fib}}_{f}(b))}}{\sum_{(w:{% \mathsf{fib}}_{f}(b))}}}\mathopen{}\left\\|{\mathsf{fib}}_{g(\mathsf{pr}_{1}w)}% ({\mathord{{{f}\mathopen{}\left({\mathsf{pr}_{2}w}\right)\mathclose{}}^{-1}}}_% {*}\mathopen{}\left({v}\right)\mathclose{})\right\\|_{n}\mathclose{}\Bigr{\\|}_{n}$
		$\displaystyle\simeq\mathopen{}\left\\|{\mathsf{fib}}_{f}(b)\right\\|_{n}% \mathclose{}$