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$ -connectedif 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$ -connectedif 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{}$ iscontractible.∎

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 anequivalence 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}$ , byLemma 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$ -connectedfamily 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 anequivalence 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, weuse 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 oftruncations, it suffices to give a map $\\mathsf{back}:B\\to{\\mathopen{}\\left\\|A\\right\\|_{n}\\mathclose{}}$ . We candefine 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 itsfirst component has type $\\mathopen{}\\left\\|{\\mathsf{fib}}_{f}(y)\\right\\|_{n}\\mathclose{}$ , and we can obtain anelement 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 tocover 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 theresult.

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 wewant is essentially the second component of the ${\\mathsf{fib}}_{f}(y)$ , but weneed 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 toprove $P(\\mathopen{}\\left|a\\right|_{n}\\mathclose{})$ for all $a : A$ and $b:B(a)$ . Applying thisprinciple 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.