8.6 The Freudenthal suspension theorem

Before proving the Freudenthal suspension theorem, we need some auxiliary lemmas about connectedness. In \autorefcha:hlevels we proved a number of facts about $n$ -connected maps and $n$ -types for fixed $n$ ; here we are now interested in what happens when we vary $n$ . For instance, in \autorefprop:nconnected_tested_by_lv_n_dependent types we showed that $n$ -connected maps are characterized by an “induction principle” relative to families of $n$ -types. If we want to “induct along” an $n$ -connected map into a family of $k$ -types for $k>n$ , we don’t immediately know that there is a function by such an induction principle, but the following lemma says that at least our ignorance can be quantified.

Lemma 8.6.1.

If $f:A\to B$ is $n$ -connected and $P:B\to{k}\text{-}\mathsf{Type}$ is a family of $k$ -types for $k\geq n$ , then the induced function

(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\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{)}

is $(k-n-2)$ -truncated.

Proof.

We induct on the natural number $k-n$ . When $k=n$ , this is \autorefprop:nconnected_tested_by_lv_n_dependent types. For the inductive step, suppose $f$ is $n$ -connected and $P$ is a family of $k+1$ -types. To show that $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ f)$ is $(k-n-1)$ -truncated, let $k:\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)$ ; then we have

{\mathsf{fib}}_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ f)}(k)\simeq% \mathchoice{\sum_{(g:\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))}% \,}{\mathchoice{{\textstyle\sum_{(g:\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))}}}{\sum_{(g:\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))}}{\sum_{(g:\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))}}{\sum_{(g:\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))}}}{\mathchoice{{\textstyle\sum_{(g:\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))}}}{\sum_{(g:\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))}}{\sum_{(g:\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))}}{\sum_{(g:\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))}}}{\mathchoice{{\textstyle\sum_{(g:\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))}}}{\sum_{(g:\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))}}{\sum_{(g:\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))}}{\sum_{(g:\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))}}}\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)}}}g(f(a))=k(a).

Let $(g,p)$ and $(h,q)$ lie in this type, so $p:g\circ f\sim k$ and $q:h\circ f\sim k$ ; then we also have

\big{(}(g,p)=(h,q)\big{)}\simeq\Bigl{(}\mathchoice{\sum_{r:g\sim h}\,}{% \mathchoice{{\textstyle\sum_{(r:g\sim h)}}}{\sum_{(r:g\sim h)}}{\sum_{(r:g\sim h% )}}{\sum_{(r:g\sim h)}}}{\mathchoice{{\textstyle\sum_{(r:g\sim h)}}}{\sum_{(r:% g\sim h)}}{\sum_{(r:g\sim h)}}{\sum_{(r:g\sim h)}}}{\mathchoice{{\textstyle% \sum_{(r:g\sim h)}}}{\sum_{(r:g\sim h)}}{\sum_{(r:g\sim h)}}{\sum_{(r:g\sim h)% }}}r\circ f=p\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}% }}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{{q}^{-1}}\Bigr{)}.

However, here the right-hand side is a fiber of the map

(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\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)}}}Q(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)}}}Q(f(a))\Bigr{)}

where $Q(b):\!\!\equiv(g(b)=h(b))$ . Since $P$ is a family of $(k+1)$ -types, $Q$ is a family of $k$ -types, so the inductive hypothesis implies that this fiber is a $(k-n-2)$ -type. Thus, all path spaces of ${\mathsf{fib}}_{(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ f)}(k)$ are $(k-n-2)$ -types, so it is a $(k-n-1)$ -type. ∎

Recall that if ${\mathopen{}(A,a_{0})\mathclose{}}$ and ${\mathopen{}(B,b_{0})\mathclose{}}$ are pointed types, then their wedge $A\vee B$ is defined to be the pushout of $A\xleftarrow{a_{0}}\mathbf{1}\xrightarrow{b_{0}}B$ . There is a canonical map $i:A\vee B\to A\times B$ defined by the two maps ${\lambda}a.\,(a,b_{0})$ and ${\lambda}b.\,(a_{0},b)$ ; the following lemma essentially says that this map is highly connected if $A$ and $B$ are so. It is a bit more convenient both to prove and use, however, if we use the characterization of connectedness from \autorefprop:nconnected_tested_by_lv_n_dependent types and substitute in the universal property of the wedge (generalized to type families).

Lemma 8.6.2 (Wedge connectivity lemma).

Suppose that ${\mathopen{}(A,a_{0})\mathclose{}}$ and ${\mathopen{}(B,b_{0})\mathclose{}}$ are $n$ - and $m$ -connected pointed types, respectively, with $n,m\geq 0$ , and let $P:A\to B\to{(n+m)}\text{-}\mathsf{Type}.$ Then for any ${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,b_{0})}$ and ${g:\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(a_{0},b)}$ with $p:f(a_{0})=g(b_{0})$ , there exists $h:\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_{(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(a,b)$ with homotopies

q:\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)}}}h(a,b_{0})=f(a)\qquad\text% {and}\qquad r:\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)}}}h(a_{0},b)=g(b)

such that $p=\mathord{{q(a_{0})}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}r(b_{0})$ .

Proof.

Define $P:A\to\mathcal{U}$ by

P(a):\!\!\equiv\mathchoice{\sum_{k:\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(a,b)}\,}{\mathchoice{{\textstyle\sum_{(k:\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(a,b))}}}{\sum_{(k:\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(a,b))}}{\sum_{(k:\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(a,b))}}{\sum_{(k:\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(a,b))}}}{\mathchoice{{\textstyle\sum_{(k:\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(a,b))}}}{\sum_{(k:\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(a,b))}}{\sum_{(k:\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(a,b))}}{\sum_{(k:\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(a,b))}}}{\mathchoice{{\textstyle\sum_{(k:\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(a,b))}}}{\sum_{(k:\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(a,b))}}{\sum_{(k:\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(a,b))}}{\sum_{(k:\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(a,b))}}}(f(a)=k(b_{0})).

Then we have $(g,p):P(a_{0})$ . Since $a_{0}:\mathbf{1}\to A$ is $(n-1)$ -connected, if $P$ is a family of $(n-1)$ -types then we will have $\ell:\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 $\ell(a_{0})=(g,p)$ , in which case we can define $h(a,b):\!\!\equiv\mathsf{pr}_{1}(\ell(a))(b)$ . However, for fixed $a$ , the type $P(a)$ is the fiber over $f(a)$ of the map

\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(a,b)\Bigr{)}\to P% (a,b_{0})

given by precomposition with $b_{0}:\mathbf{1}\to B$ . Since $b_{0}:\mathbf{1}\to B$ is $(m-1)$ -connected, for this fiber to be $(n-1)$ -connected, by \autorefthm:conn-trunc-variable-ind it suffices for each type $P(a,b)$ to be an $(n+m)$ -type, which we have assumed. ∎

Let $(X,x_{0})$ be a pointed type, and recall the definition of the suspension $\Sigma X$ from \autorefsec:suspension, with constructors $\mathsf{N},\mathsf{S}:\Sigma X$ and $\mathsf{merid}:X\to(\mathsf{N}=\mathsf{S})$ . We regard $\Sigma X$ as a pointed space with basepoint $\mathsf{N}$ , so that we have $\Omega\Sigma X:\!\!\equiv(\mathsf{N}=_{\Sigma X}\mathsf{N})$ . Then there is a canonical map

	$\displaystyle\sigma$	$\displaystyle:X\to\Omega\Sigma X$
	$\displaystyle\sigma(x)$	$\displaystyle:\!\!\equiv\mathsf{merid}(x)\mathchoice{\mathbin{\raisebox{2.15pt% }{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}% ^{-1}}.$

Remark 8.6.3.

In classical algebraic topology, one considers the reduced suspension, in which the path $\mathsf{merid}(x_{0})$ is collapsed down to a point, identifying $\mathsf{N}$ and $\mathsf{S}$ . The reduced and unreduced suspensions are homotopy equivalent, so the distinction is invisible to our purely homotopy-theoretic eyes — and higher inductive types only allow us to “identify” points up to a higher path anyway, there is no purpose to considering reduced suspensions in homotopy type theory. However, the “unreducedness” of our suspension is the reason for the (possibly unexpected) appearance of $\mathord{{\mathsf{merid}(x_{0})}^{-1}}$ in the definition of $\sigma$ .

Our goal is now to prove the following.

Theorem 8.6.4 (The Freudenthal suspension theorem).

Suppose that $X$ is $n$ -connected and pointed, with $n\geq 0$ . Then the map $\sigma:X\to\Omega\Sigma(X)$ is $2n$ -connected.

We will use the encode-decode method, but applied in a slightly different way. In most cases so far, we have used it to characterize the loop space $\Omega(A,a_{0})$ of some type as equivalent to some other type $B$ , by constructing a family $\mathsf{code}:A\to\mathcal{U}$ with $\mathsf{code}(a_{0}):\!\!\equiv B$ and a family of equivalences $\mathsf{decode}:\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)}}}\mathsf% {code}(x)\simeq(a_{0}=x)$ .

In this case, however, we want to show that $\sigma:X\to\Omega\Sigma X$ is $2n$ -connected. We could use a truncated version of the previous method, such as we will see in \autorefsec:van-kampen, to prove that $\mathopen{}\left\|X\right\|_{2n}\mathclose{}\to\mathopen{}\left\|\Omega\Sigma X% \right\|_{2n}\mathclose{}$ is an equivalence—but this is a slightly weaker statement than the map being $2n$ -connected (see \autorefthm:conn-pik,\autorefthm:pik-conn). However, note that in the general case, to prove that $\mathsf{decode}(x)$ is an equivalence, we could equivalently be proving that its fibers are contractible, and we would still be able to use induction over the base type. This we can generalize to prove connectedness of a map into a loop space, i.e. that the truncations of its fibers are contractible. Moreover, instead of constructing $\mathsf{code}$ and $\mathsf{decode}$ separately, we can construct directly a family of codes for the truncations of the fibers.

Definition 8.6.5.

If $X$ is $n$ -connected and pointed with $n\geq 0$ , then there is a family

\mathsf{code}:\mathchoice{\prod_{y:\Sigma X}\,}{\mathchoice{{\textstyle\prod_{% (y:\Sigma X)}}}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X% )}}}{\mathchoice{{\textstyle\prod_{(y:\Sigma X)}}}{\prod_{(y:\Sigma X)}}{\prod% _{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}}{\mathchoice{{\textstyle\prod_{(y:% \Sigma X)}}}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}% }(\mathsf{N}=y)\to\mathcal{U}

(8.6.5)

such that

	$\displaystyle\mathsf{code}(\mathsf{N},p)$	$\displaystyle:\!\!\equiv\mathopen{}\left\\|{\mathsf{fib}}_{\sigma}(p)\right\\|_{% 2n}\mathclose{}\equiv\mathopen{}\left\\|\mathchoice{{\textstyle\sum_{(x:X)}}}{% \sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}(\mathsf{merid}(x)\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{% \mathsf{merid}(x_{0})}^{-1}}=p)\right\\|_{2n}\mathclose{}$		(8.6.6)
	$\displaystyle\mathsf{code}(\mathsf{S},q)$	$\displaystyle:\!\!\equiv\mathopen{}\left\\|{\mathsf{fib}}_{\mathsf{merid}}(q)% \right\\|_{2n}\mathclose{}\equiv\mathopen{}\left\\|\mathchoice{{\textstyle\sum_{% (x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}}(\mathsf{merid}(x)=q)\right% \\|_{2n}\mathclose{}.$		(8.6.6)

Our eventual goal will be to prove that $\mathsf{code}(y,p)$ is contractible for all $y:\Sigma X$ and $p:\mathsf{N}=y$ . Applying this with $y:\!\!\equiv\mathsf{N}$ will show that all fibers of $\sigma$ are $2n$ -connected, and thus $\sigma$ is $2n$ -connected.

Proof of \autorefthm:freudcode.

We define $\mathsf{code}(y,p)$ by induction on $y:\Sigma X$ , where the first two cases are (8.6.6) and (8.6.6). It remains to construct, for each $x_{1}:X$ , a dependent path

\mathsf{code}(\mathsf{N})=^{{\lambda}y.\,(\mathsf{N}=y)\to\mathcal{U}}_{% \mathsf{merid}(x_{1})}\mathsf{code}(\mathsf{S}).

By \autorefthm:dpath-arrow, this is equivalent to giving a family of paths

\mathchoice{\prod_{q:\mathsf{N}=\mathsf{S}}\,}{\mathchoice{{\textstyle\prod_{(% q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:% \mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\mathchoice{{% \textstyle\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N}=\mathsf{S})% }}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}}{% \mathchoice{{\textstyle\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N% }=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=% \mathsf{S})}}}\mathsf{code}(\mathsf{N})(\mathsf{transport}^{{\lambda}y.\,(% \mathsf{N}=y)}(\mathord{{\mathsf{merid}(x_{1})}^{-1}},q))=\mathsf{code}(% \mathsf{S})(q).

And by univalence and transport in path types, this is equivalent to a family of equivalences

\mathchoice{\prod_{q:\mathsf{N}=\mathsf{S}}\,}{\mathchoice{{\textstyle\prod_{(% q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:% \mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\mathchoice{{% \textstyle\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N}=\mathsf{S})% }}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}}{% \mathchoice{{\textstyle\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N% }=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=% \mathsf{S})}}}\mathsf{code}(\mathsf{N},q\mathchoice{\mathbin{\raisebox{2.15pt}% {$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{1})}% ^{-1}})\simeq\mathsf{code}(\mathsf{S},q).

We will define a family of maps

\mathchoice{\prod_{q:\mathsf{N}=\mathsf{S}}\,}{\mathchoice{{\textstyle\prod_{(% q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:% \mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\mathchoice{{% \textstyle\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N}=\mathsf{S})% }}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}}{% \mathchoice{{\textstyle\prod_{(q:\mathsf{N}=\mathsf{S})}}}{\prod_{(q:\mathsf{N% }=\mathsf{S})}}{\prod_{(q:\mathsf{N}=\mathsf{S})}}{\prod_{(q:\mathsf{N}=% \mathsf{S})}}}\mathsf{code}(\mathsf{N},q\mathchoice{\mathbin{\raisebox{2.15pt}% {$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{1})}% ^{-1}})\to\mathsf{code}(\mathsf{S},q).

(8.6.7)

and then show that they are all equivalences. Thus, let $q:\mathsf{N}=\mathsf{S}$ ; by the universal property of truncation and the definitions of $\mathsf{code}(\mathsf{N},\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ and $\mathsf{code}(\mathsf{S},\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ , it will suffice to define for each $x_{2}:X$ , a map

\big{(}\mathsf{merid}(x_{2})\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}% ^{-1}}=q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{1})}^{-1}}\big{)}\to\mathopen{}% \left\|\mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_% {(x:X)}}(\mathsf{merid}(x)=q)\right\|_{2n}\mathclose{}.

Now for each $x_{1},x_{2}:X$ , this type is $2n$ -truncated, while $X$ is $n$ -connected. Thus, by \autorefthm:wedge-connectivity, it suffices to define this map when $x_{1}$ is $x_{0}$ , when $x_{2}$ is $x_{0}$ , and check that they agree when both are $x_{0}$ .

When $x_{1}$ is $x_{0}$ , the hypothesis is $r:\mathsf{merid}(x_{2})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}=q% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}$ . Thus, by canceling $\mathord{{\mathsf{merid}(x_{0})}^{-1}}$ from $r$ to get $r^{\prime}:\mathsf{merid}(x_{2})=q$ , so we can define the image to be $\mathopen{}\left|(x_{2},r^{\prime})\right|_{2n}\mathclose{}$ .

When $x_{2}$ is $x_{0}$ , the hypothesis is $r:\mathsf{merid}(x_{0})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}=q% \mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathord{{\mathsf{merid}(x_{1})}^{-1}}$ . Rearranging this, we obtain $r^{\prime\prime}:\mathsf{merid}(x_{1})=q$ , and we can define the image to be $\mathopen{}\left|(x_{1},r^{\prime\prime})\right|_{2n}\mathclose{}$ .

Finally, when both $x_{1}$ and $x_{2}$ are $x_{0}$ , it suffices to show the resulting $r^{\prime}$ and $r^{\prime\prime}$ agree; this is an easy lemma about path composition. This completes the definition of (8.6.7). To show that it is a family of equivalences, since being an equivalence is a mere proposition and $x_{0}:\mathbf{1}\to X$ is (at least) $(-1)$ -connected, it suffices to assume $x_{1}$ is $x_{0}$ . In this case, inspecting the above construction we see that it is essentially the $2n$ -truncation of the function that cancels $\mathord{{\mathsf{merid}(x_{0})}^{-1}}$ , which is an equivalence. ∎

In addition to (8.6.6) and (8.6.6), we will need to extract from the construction of $\mathsf{code}$ some information about how it acts on paths. For this we use the following lemma.

Lemma 8.6.8.

Let $A:\mathcal{U}$ , $B:A\to\mathcal{U}$ , and $C:\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)}}}B(a)\to\mathcal{U}$ , and also $a_{1},a_{2}:A$ with $m:a_{1}=a_{2}$ and $b:B(a_{2})$ . Then the function

\mathsf{transport}^{\widehat{C}}(\mathsf{pair}^{\mathord{=}}(m,t),\mathord{% \hskip 1.0pt\text{--}\hskip 1.0pt}):C(a_{1},\mathsf{transport}^{B}(\mathord{{m% }^{-1}},b))\to C(a_{2},b),

where $t:\mathsf{transport}^{B}(m,\mathsf{transport}^{B}(\mathord{{m}^{-1}},b))=b$ is the obvious coherence path and $\widehat{C}:(\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)}}}B(a))\to\mathcal{U}$ is the uncurried form of $C$ , is equal to the equivalence obtained by univalence from the composite

	$\displaystyle C(a_{1},\mathsf{transport}^{B}(\mathord{{m}^{-1}},b))$	$\displaystyle=\mathsf{transport}^{{\lambda}a.\,B(a)\to\mathcal{U}}(m,C(a_{1}))% (b){}$		(by \eqref{eq:transport-arrow})
		$\displaystyle=C(a_{2},b).{}$		(by $\mathsf{happly}(\mathsf{apd}_{C}\mathopen{}\left(m\right)\mathclose{},b)$)

Proof.

By path induction, we may assume $a_{2}$ is $a_{1}$ and $m$ is $\mathsf{refl}_{a_{1}}$ , in which case both functions are the identity. ∎

We apply this lemma with $A:\!\!\equiv\Sigma X$ and $B:\!\!\equiv{\lambda}y.\,(\mathsf{N}=y)$ and $C:\!\!\equiv\mathsf{code}$ , while $a_{1}:\!\!\equiv\mathsf{N}$ and $a_{2}:\!\!\equiv\mathsf{S}$ and $m:\!\!\equiv\mathsf{merid}(x_{1})$ for some $x_{1}:X$ , and finally $b:\!\!\equiv q$ is some path $\mathsf{N}=\mathsf{S}$ . The computation rule for induction over $\Sigma X$ identifies $\mathsf{apd}_{C}\mathopen{}\left(m\right)\mathclose{}$ with a path constructed in a certain way out of univalence and function extensionality. The second function described in \autorefthm:freudlemma essentially consists of undoing these applications of univalence and function extensionality, reducing back to the particular functions (8.6.7) that we defined using \autorefthm:wedge-connectivity. Therefore, \autorefthm:freudlemma says that transporting along $\mathsf{pair}^{\mathord{=}}(q,t)$ essentially recovers these functions.

Finally, by construction, when $x_{1}$ or $x_{2}$ coincides with $x_{0}$ and the input is in the image of $\mathopen{}\left|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\right|_{2n}% \mathclose{}$ , we know more explicitly what these functions are. Thus, for any $x_{2}:X$ , we have

\mathsf{transport}^{\hat{\mathsf{code}}}(\mathsf{pair}^{\mathord{=}}(\mathsf{% merid}(x_{0}),t),\mathopen{}\left|(x_{2},r)\right|_{2n}\mathclose{})=\mathopen% {}\left|(x_{1},r^{\prime})\right|_{2n}\mathclose{}

(8.6.9)

where $r:\mathsf{merid}(x_{2})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}=% \mathsf{transport}^{B}(\mathord{{\mathsf{merid}(x_{0})}^{-1}},q)$ is arbitrary as before, and $r^{\prime}:\mathsf{merid}(x_{2})=q$ is obtained from $r$ by identifying its end point with $q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}$ and canceling $\mathord{{\mathsf{merid}(x_{0})}^{-1}}$ . Similarly, for any $x_{1}:X$ , we have

\mathsf{transport}^{\hat{\mathsf{code}}}(\mathsf{pair}^{\mathord{=}}(\mathsf{% merid}(x_{1}),t),\mathopen{}\left|(x_{0},r)\right|_{2n}\mathclose{})=\mathopen% {}\left|(x_{1},r^{\prime\prime})\right|_{2n}\mathclose{}

(8.6.10)

where $r:\mathsf{merid}(x_{0})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}=% \mathsf{transport}^{B}(\mathord{{\mathsf{merid}(x_{1})}^{-1}},q)$ , and $r^{\prime\prime}:\mathsf{merid}(x_{1})=q$ is obtained by identifying its end point and rearranging paths.

Proof of \autorefthm:freudenthal.

It remains to show that $\mathsf{code}(y,p)$ is contractible for each $y:\Sigma X$ and $p:\mathsf{N}=y$ . First we must choose a center of contraction, say $c(y,p):\mathsf{code}(y,p)$ . This corresponds to the definition of the function $\mathsf{encode}$ in our previous proofs, so we define it by transport. Note that in the special case when $y$ is $\mathsf{N}$ and $p$ is $\mathsf{refl}_{\mathsf{N}}$ , we have

\mathsf{code}(\mathsf{N},\mathsf{refl}_{\mathsf{N}})\equiv\mathopen{}\left\|% \mathchoice{{\textstyle\sum_{(x:X)}}}{\sum_{(x:X)}}{\sum_{(x:X)}}{\sum_{(x:X)}% }(\mathsf{merid}(x)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}=% \mathsf{refl}_{\mathsf{N}})\right\|_{2n}\mathclose{}.

Thus, we can choose $c(\mathsf{N},\mathsf{refl}_{\mathsf{N}}):\!\!\equiv\mathopen{}\left|(x_{0},% \mathsf{rinv}_{\mathsf{merid}(x_{0})})\right|_{2n}\mathclose{}$ , where $\mathrm{rinv}_{q}$ is the obvious path $q\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{% \raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,% \centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$% }}}\mathord{{q}^{-1}}=\mathsf{refl}$ for any $q$ . We can now obtain $c:\mathchoice{\prod_{(y:\Sigma X)}\,}{\mathchoice{{\textstyle\prod_{(y:\Sigma X% )}}}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}}{% \mathchoice{{\textstyle\prod_{(y:\Sigma X)}}}{\prod_{(y:\Sigma X)}}{\prod_{(y:% \Sigma X)}}{\prod_{(y:\Sigma X)}}}{\mathchoice{{\textstyle\prod_{(y:\Sigma X)}% }}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}{\prod_{(y:\Sigma X)}}}% \mathchoice{\prod_{(p:\mathsf{N}=y)}\,}{\mathchoice{{\textstyle\prod_{(p:% \mathsf{N}=y)}}}{\prod_{(p:\mathsf{N}=y)}}{\prod_{(p:\mathsf{N}=y)}}{\prod_{(p% :\mathsf{N}=y)}}}{\mathchoice{{\textstyle\prod_{(p:\mathsf{N}=y)}}}{\prod_{(p:% \mathsf{N}=y)}}{\prod_{(p:\mathsf{N}=y)}}{\prod_{(p:\mathsf{N}=y)}}}{% \mathchoice{{\textstyle\prod_{(p:\mathsf{N}=y)}}}{\prod_{(p:\mathsf{N}=y)}}{% \prod_{(p:\mathsf{N}=y)}}{\prod_{(p:\mathsf{N}=y)}}}\mathsf{code}(y,p)$ by path induction on $p$ , but it will be important below that we can also give a concrete definition in terms of transport:

c(y,p):\!\!\equiv\mathsf{transport}^{\hat{\mathsf{code}}}(\mathsf{pair}^{% \mathord{=}}(p,\mathsf{tid}_{p}),c(\mathsf{N},\mathsf{refl}_{\mathsf{N}}))

where $\hat{\mathsf{code}}:\big{(}\mathchoice{\sum_{y:\Sigma X}\,}{\mathchoice{{% \textstyle\sum_{(y:\Sigma X)}}}{\sum_{(y:\Sigma X)}}{\sum_{(y:\Sigma X)}}{\sum% _{(y:\Sigma X)}}}{\mathchoice{{\textstyle\sum_{(y:\Sigma X)}}}{\sum_{(y:\Sigma X% )}}{\sum_{(y:\Sigma X)}}{\sum_{(y:\Sigma X)}}}{\mathchoice{{\textstyle\sum_{(y% :\Sigma X)}}}{\sum_{(y:\Sigma X)}}{\sum_{(y:\Sigma X)}}{\sum_{(y:\Sigma X)}}}(% \mathsf{N}=y)\big{)}\to\mathcal{U}$ is the uncurried version of $\mathsf{code}$ , and $\mathsf{tid}_{p}:{p}_{*}\mathopen{}\left({\mathsf{refl}}\right)\mathclose{}=p$ is a standard lemma.

Next, we must show that every element of $\mathsf{code}(y,p)$ is equal to $c(y,p)$ . Again, by path induction, it suffices to assume $y$ is $\mathsf{N}$ and $p$ is $\mathsf{refl}_{\mathsf{N}}$ . In fact, we will prove it more generally when $y$ is $\mathsf{N}$ and $p$ is arbitrary. That is, we will show that for any $p:\mathsf{N}=\mathsf{N}$ and $d:\mathsf{code}(\mathsf{N},p)$ we have $d=c(\mathsf{N},p)$ . Since this equality is a $(2n-1)$ -type, we may assume $d$ is of the form $\mathopen{}\left|(x_{1},r)\right|_{2n}\mathclose{}$ for some $x_{1}:X$ and $r:\mathsf{merid}(x_{1})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}=p$ .

Now by a further path induction, we may assume that $r$ is reflexivity, and $p$ is $\mathsf{merid}(x_{1})\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}^{-1}}$ . (This is why we generalized to arbitrary $p$ above.) Thus, we have to prove that

\mathopen{}\left|(x_{1},\mathsf{refl}_{\mathsf{merid}(x_{1})\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{% \mathsf{merid}(x_{0})}^{-1}}})\right|_{2n}\mathclose{}\;=\;c\left(\mathsf{N},% \mathsf{refl}_{\mathsf{merid}(x_{1})\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}% ^{-1}}}\right).

(8.6.11)

By definition, the right-hand side of this equality is

\displaystyle\mathsf{transport}^{\hat{\mathsf{code}}}\Big{(}\mathsf{pair}^{% \mathord{=}}(\mathsf{merid}(x_{1})\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\mathord{{\mathsf{merid}(x_{0})}% ^{-1}},\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}),\,\mathopen% {}\left|(x_{0},\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt})% \right|_{2n}\mathclose{}\Big{)}\\ \displaystyle=\mathsf{transport}^{\hat{\mathsf{code}}}\begin{aligned} % \displaystyle\Big{(}&\displaystyle{\mathsf{pair}^{\mathord{=}}(\mathord{{% \mathsf{merid}(x_{0})}^{-1}},\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}% \hskip 1.0pt})},\\ &\displaystyle{\mathsf{transport}^{\hat{\mathsf{code}}}\Big{(}\mathsf{pair}^{% \mathord{=}}(\mathsf{merid}(x_{1}),\mathord{\hskip 1.0pt\underline{\hskip 4.3% pt}\hskip 1.0pt}),\,\mathopen{}\left|(x_{0},\mathord{\hskip 1.0pt\underline{% \hskip 4.3pt}\hskip 1.0pt})\right|_{2n}\mathclose{}\Big{)}}\Big{)}\end{aligned% }\\ \displaystyle=\mathsf{transport}^{\hat{\mathsf{code}}}\Big{(}\mathsf{pair}^{% \mathord{=}}(\mathord{{\mathsf{merid}(x_{0})}^{-1}},\mathord{\hskip 1.0pt% \underline{\hskip 4.3pt}\hskip 1.0pt}),\,\mathopen{}\left|(x_{1},\mathord{% \hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt})\right|_{2n}\mathclose{}\Big% {)}=\mathopen{}\left|(x_{1},\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}% \hskip 1.0pt})\right|_{2n}\mathclose{}

where the underscore $\mathord{\hskip 1.0pt\underline{\hskip 4.3pt}\hskip 1.0pt}$ ought to be filled in with suitable coherence paths. Here the first step is functoriality of transport, the second invokes (8.6.10), and the third invokes (8.6.9) (with transport moved to the other side). Thus we have the same first component as the left-hand side of (8.6.11). We leave it to the reader to verify that the coherence paths all cancel, giving reflexivity in the second component. ∎

Corollary 8.6.12 (Freudenthal Equivalence).

Suppose that $X$ is $n$ -connected and pointed, with $n\geq 0$ . Then $\mathopen{}\left\|X\right\|_{2n}\mathclose{}\simeq\mathopen{}\left\|\Omega% \Sigma(X)\right\|_{2n}\mathclose{}$ .

Proof.

By \crefthm:freudenthal, $\sigma$ is $2n$ -connected. By \creflem:connected-map-equiv-truncation, it is therefore an equivalence on $2n$ -truncations. ∎

One important corollary of the Freudenthal suspension theorem is that the homotopy groups of spheres are stable in a certain range (these are the northeast-to-southwest diagonals in \autoreftab:homotopy-groups-of-spheres):

Corollary 8.6.13 (Stability for Spheres).

If $k\leq 2n-2$ , then $\pi_{k+1}(S^{n+1})=\pi_{k}(S^{n})$ .

Proof.

Assume $k\leq 2n-2$ . By \crefcor:sn-connected, $\mathbb{S}^{n}$ is $(n-1)$ -connected. Therefore, by \crefcor:freudenthal-equiv,

\mathopen{}\left\|\Omega(\Sigma(\mathbb{S}^{n}))\right\|_{2(n-1)}\mathclose{}=% \mathopen{}\left\|\mathbb{S}^{n}\right\|_{2(n-1)}\mathclose{}.

By \creflem:truncation-le, because $k\leq 2(n-1)$ , applying $\mathopen{}\left\|\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\right\|_{k}% \mathclose{}$ to both sides shows that this equation holds for $k$ :

\mathopen{}\left\|\Omega(\Sigma(\mathbb{S}^{n}))\right\|_{k}\mathclose{}=% \mathopen{}\left\|\mathbb{S}^{n}\right\|_{k}\mathclose{}.

(8.6.14)

Then, the main idea of the proof is as follows; we omit checking that these equivalences act appropriately on the base points of these spaces:

$\displaystyle\pi_{k+1}(\mathbb{S}^{n+1})$	$\displaystyle\equiv\mathopen{}\left\\|\Omega^{k+1}(\mathbb{S}^{n+1})\right\\|_{0% }\mathclose{}$
	$\displaystyle\equiv\mathopen{}\left\\|\Omega^{k}(\Omega(\mathbb{S}^{n+1}))% \right\\|_{0}\mathclose{}$
	$\displaystyle\equiv\mathopen{}\left\\|\Omega^{k}(\Omega(\Sigma(\mathbb{S}^{n}))% )\right\\|_{0}\mathclose{}$
	$\displaystyle=\Omega^{k}(\mathopen{}\left\\|(\Omega(\Sigma(\mathbb{S}^{n})))% \right\\|_{k}\mathclose{}){}$	(by \autorefthm:path-truncation)
	$\displaystyle=\Omega^{k}(\mathopen{}\left\\|\mathbb{S}^{n}\right\\|_{k}% \mathclose{}){}$	(by \eqref{eq:freudenthal-for-spheres})
	$\displaystyle=\mathopen{}\left\\|\Omega^{k}(\mathbb{S}^{n})\right\\|_{0}% \mathclose{}{}$	(by \autorefthm:path-truncation)
	$\displaystyle\equiv\pi_{k}(\mathbb{S}^{n}).\qed$

This means that once we have calculated one entry in one of these stable diagonals, we know all of them. For example:

Theorem 8.6.15.

$\pi_{n}(\mathbb{S}^{n})=\mathbb{Z}$ for every $n\geq 1$ .

Proof.

The proof is by induction on $n$ . We already have $\pi_{1}(\mathbb{S}^{1})=\mathbb{Z}$ (\autorefcor:pi1s1) and $\pi_{2}(\mathbb{S}^{2})=\mathbb{Z}$ (\autorefcor:pis2-hopf). When $n\geq 2$ , $n\leq(2n-2)$ . Therefore, by \crefcor:stability-spheres, $\pi_{n+1}(S^{n+1})=\pi_{n}(S^{n})$ , and this equivalence, combined with the inductive hypothesis, gives the result. ∎

Corollary 8.6.16.

$\mathbb{S}^{n+1}$ is not an $n$ -type for any $n\geq-1$ .

Title	8.6 The Freudenthal suspension theorem
\metatable

$\displaystyle\pi_{k+1}(\mathbb{S}^{n+1})$	$\displaystyle\equiv\mathopen{}\left\\|\Omega^{k+1}(\mathbb{S}^{n+1})\right\\|_{0% }\mathclose{}$
	$\displaystyle\equiv\mathopen{}\left\\|\Omega^{k}(\Omega(\mathbb{S}^{n+1}))% \right\\|_{0}\mathclose{}$
	$\displaystyle\equiv\mathopen{}\left\\|\Omega^{k}(\Omega(\Sigma(\mathbb{S}^{n}))% )\right\\|_{0}\mathclose{}$
	$\displaystyle=\Omega^{k}(\mathopen{}\left\\|(\Omega(\Sigma(\mathbb{S}^{n})))% \right\\|_{k}\mathclose{}){}$	(by \autorefthm:path-truncation)
	$\displaystyle=\Omega^{k}(\mathopen{}\left\\|\mathbb{S}^{n}\right\\|_{k}% \mathclose{}){}$	(by \eqref{eq:freudenthal-for-spheres})
	$\displaystyle=\mathopen{}\left\\|\Omega^{k}(\mathbb{S}^{n})\right\\|_{0}% \mathclose{}{}$	(by \autorefthm:path-truncation)
	$\displaystyle\equiv\pi_{k}(\mathbb{S}^{n}).\qed$