# 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. 1.

$f$ is $n$-connected.

2. 2.

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

3. 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