# 8.2 Connectedness of suspensions

Recall from \autorefsec:connectivity that a type $A$ is called $n$-connected if $\mathopen{}\left\|A\right\|_{n}\mathclose{}$ is contractible. The aim of this section is to prove that the operation of suspension from \autorefsec:suspension increases connectedness.

###### Theorem 8.2.1.

If $A$ is $n$-connected then the suspension of $A$ is $(n+1)$-connected.

###### Proof.

We remarked in \autorefsec:colimits that the suspension of $A$ is the pushout $\mathbf{1}\sqcup^{A}\mathbf{1}$, so we need to prove that the following type is contractible:

 $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}.$

By \autorefreflectcommutespushout we know that $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}$ is a pushout in ${(n+1)}\text{-}\mathsf{Type}$ of the diagram

 $\xymatrix{\mathopen{}\left\|A\right\|_{n+1}\mathclose{}\ar[d]\ar[r]&\mathopen{% }\left\|\mathbf{1}\right\|_{n+1}\mathclose{}\\ \mathopen{}\left\|\mathbf{1}\right\|_{n+1}\mathclose{}&}.$

Given that $\mathopen{}\left\|\mathbf{1}\right\|_{n+1}\mathclose{}=\mathbf{1}$, the type $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}$ is also a pushout of the following diagram in ${(n+1)}\text{-}\mathsf{Type}$ (because both diagrams are equal)

 $\mathscr{D}=\vbox{\xymatrix{\mathopen{}\left\|A\right\|_{n+1}\mathclose{} \ar[% d] \ar[r] & \mathbf{1} \\ \mathbf{1} & }}.$

We will now prove that $\mathbf{1}$ is also a pushout of $\mathscr{D}$ in ${(n+1)}\text{-}\mathsf{Type}$. Let $E$ be an $(n+1)$-truncated type; we need to prove that the following map is an equivalence

 $\left\{\begin{array}[]{rcl}(\mathbf{1}\to E)&\longrightarrow&\mathsf{cocone}_{% \mathscr{D}}(E)\\ y&\longmapsto&(y,y,{\lambda}u.\,\mathsf{refl}_{y(\star)})\end{array}\right..$

where we recall that $\mathsf{cocone}_{\mathscr{D}}(E)$ is the type

 $\mathchoice{\sum_{(f:\mathbf{1}\to E)}\,}{\mathchoice{{\textstyle\sum_{(f:% \mathbf{1}\to E)}}}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}{% \sum_{(f:\mathbf{1}\to E)}}}{\mathchoice{{\textstyle\sum_{(f:\mathbf{1}\to E)}% }}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}% \to E)}}}{\mathchoice{{\textstyle\sum_{(f:\mathbf{1}\to E)}}}{\sum_{(f:\mathbf% {1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}{\sum_{(f:\mathbf{1}\to E)}}}% \mathchoice{\sum_{(g:\mathbf{1}\to E)}\,}{\mathchoice{{\textstyle\sum_{(g:% \mathbf{1}\to E)}}}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}{% \sum_{(g:\mathbf{1}\to E)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbf{1}\to E)}% }}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}% \to E)}}}{\mathchoice{{\textstyle\sum_{(g:\mathbf{1}\to E)}}}{\sum_{(g:\mathbf% {1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}{\sum_{(g:\mathbf{1}\to E)}}}(\mathopen% {}\left\|A\right\|_{n+1}\mathclose{}\to(f(\star)=_{E}{}g(\star))).$

The map $\left\{\begin{array}[]{rcl}(\mathbf{1}\to E)&\longrightarrow&E\\ f&\longmapsto&f(\star)\end{array}\right.$ is an equivalence, hence we also have

 $\mathsf{cocone}_{\mathscr{D}}(E)=\mathchoice{\sum_{(x:E)}\,}{\mathchoice{{% \textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}}}{% \mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}% }}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:% E)}}}\mathchoice{\sum_{(y:E)}\,}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum_{(% y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum% _{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{% \sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}(\mathopen{}\left\|A\right\|_{n+1}% \mathclose{}\to(x=_{E}y)).$

Now $A$ is $n$-connected hence so is $\mathopen{}\left\|A\right\|_{n+1}\mathclose{}$ because $\mathopen{}\left\|\mathopen{}\left\|A\right\|_{n+1}\mathclose{}\right\|_{n}% \mathclose{}=\mathopen{}\left\|A\right\|_{n}\mathclose{}=\mathbf{1}$, and $(x=_{E}y)$ is $n$-truncated because $E$ is $(n+1)$-connected. Hence by \autorefconnectedtotruncated the following map is an equivalence

 $\left\{\begin{array}[]{rcl}(x=_{E}y)&\longrightarrow&(\mathopen{}\left\|A% \right\|_{n+1}\mathclose{}\to(x=_{E}y))\\ p&\longmapsto&{\lambda}z.\,p\end{array}\right.$

Hence we have

 $\mathsf{cocone}_{\mathscr{D}}(E)=\mathchoice{\sum_{(x:E)}\,}{\mathchoice{{% \textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}}}{% \mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}% }}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:% E)}}}\mathchoice{\sum_{(y:E)}\,}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum_{(% y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum% _{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{% \sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}(x=_{E}y).$

But the following map is an equivalence

 $\left\{\begin{array}[]{rcl}E&\longrightarrow&\mathchoice{\sum_{(x:E)}\,}{% \mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:E)}% }}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{(x:% E)}}}{\mathchoice{{\textstyle\sum_{(x:E)}}}{\sum_{(x:E)}}{\sum_{(x:E)}}{\sum_{% (x:E)}}}\mathchoice{\sum_{(y:E)}\,}{\mathchoice{{\textstyle\sum_{(y:E)}}}{\sum% _{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}}}{% \sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}{\mathchoice{{\textstyle\sum_{(y:E)}% }}{\sum_{(y:E)}}{\sum_{(y:E)}}{\sum_{(y:E)}}}(x=_{E}y)\\ x&\longmapsto&(x,x,\mathsf{refl}_{x})\end{array}\right..$

Hence

 $\mathsf{cocone}_{\mathscr{D}}(E)=E.$

Finally we get an equivalence

 $(\mathbf{1}\to E)\simeq\mathsf{cocone}_{\mathscr{D}}(E)$

We can now unfold the definitions in order to get the explicit expression of this map, and we see easily that this is exactly the map we had at the beginning.

Hence we proved that $\mathbf{1}$ is a pushout of $\mathscr{D}$ in ${(n+1)}\text{-}\mathsf{Type}$. Using uniqueness of pushouts we get that $\mathopen{}\left\|\mathbf{1}\sqcup^{A}\mathbf{1}\right\|_{n+1}\mathclose{}=% \mathbf{1}$ which proves that the suspension of $A$ is $(n+1)$-connected. ∎

###### Corollary 8.2.2.

For all $n:\mathbb{N}$, the sphere $\mathbb{S}^{n}$ is $(n-1)$-connected.

###### Proof.

We prove this by induction on $n$. For $n=0$ we have to prove that $\mathbb{S}^{0}$ is merely inhabited, which is clear. Let $n:\mathbb{N}$ be such that $\mathbb{S}^{n}$ is $(n-1)$-connected. By definition $\mathbb{S}^{n+1}$ is the suspension of $\mathbb{S}^{n}$, hence by the previous lemma $\mathbb{S}^{n+1}$ is $n$-connected. ∎

Title 8.2 Connectedness of suspensions
\metatable