# 6.5 Suspensions

The suspension of a type $A$ is the universal way of making the points of $A$ into paths (and hence the paths in $A$ into 2-paths, and so on). It is a type $\Sigma A$ defined by the following generators:11There is an unfortunate clash of notation with dependent pair types, which of course are also written with a $\Sigma$. However, context usually disambiguates.

• a point $\mathsf{N}:\Sigma A$,

• a point $\mathsf{S}:\Sigma A$, and

• a function $\mathsf{merid}:A\to(\mathsf{N}=_{\Sigma A}\mathsf{S})$.

The names are intended to suggest a “globe” of sorts, with a north pole, a south pole, and an $A$’s worth of meridians from one to the other. Indeed, as we will see, if $A=\mathbb{S}^{1}$, then its suspension is equivalent to the surface of an ordinary sphere, $\mathbb{S}^{2}$.

The recursion principle for $\Sigma A$ says that given a type $B$ together with

• points $n,s:B$ and

• a function $m:A\to(n=s)$,

we have a function $f:\Sigma A\to B$ such that $f(\mathsf{N})\equiv n$ and $f(\mathsf{S})\equiv s$, and for all $a:A$ we have ${f}\mathopen{}\left({\mathsf{merid}(a)}\right)\mathclose{}=m(a)$. Similarly, the induction principle says that given $P:\Sigma A\to\mathcal{U}$ together with

• a point $n:P(\mathsf{N})$,

• a point $s:P(\mathsf{S})$, and

• for each $a:A$, a path $m(a):n=^{P}_{\mathsf{merid}(a)}s$,

there exists a function $f:\mathchoice{\prod_{x:\Sigma A}\,}{\mathchoice{{\textstyle\prod_{(x:\Sigma A)% }}}{\prod_{(x:\Sigma A)}}{\prod_{(x:\Sigma A)}}{\prod_{(x:\Sigma A)}}}{% \mathchoice{{\textstyle\prod_{(x:\Sigma A)}}}{\prod_{(x:\Sigma A)}}{\prod_{(x:% \Sigma A)}}{\prod_{(x:\Sigma A)}}}{\mathchoice{{\textstyle\prod_{(x:\Sigma A)}% }}{\prod_{(x:\Sigma A)}}{\prod_{(x:\Sigma A)}}{\prod_{(x:\Sigma A)}}}P(x)$ such that $f(\mathsf{N})\equiv n$ and $f(\mathsf{S})\equiv s$ and for each $a:A$ we have $\mathsf{apd}_{f}\mathopen{}\left(\mathsf{merid}(a)\right)\mathclose{}=m(a)$.

Our first observation about suspension is that it gives another way to define the circle.

###### Lemma 6.5.1.

$\Sigma\mathbf{2}\simeq\mathbb{S}^{1}$.

###### Proof.

Define $f:\Sigma\mathbf{2}\to\mathbb{S}^{1}$ by recursion such that $f(\mathsf{N}):\!\!\equiv\mathsf{base}$ and $f(\mathsf{S}):\!\!\equiv\mathsf{base}$, while ${f}\mathopen{}\left({\mathsf{merid}({0_{\mathbf{2}}})}\right)\mathclose{}:=% \mathsf{loop}$ but ${f}\mathopen{}\left({\mathsf{merid}({1_{\mathbf{2}}})}\right)\mathclose{}:=% \mathsf{refl}_{\mathsf{base}}$. Define $g:\mathbb{S}^{1}\to\Sigma\mathbf{2}$ by recursion such that $g(\mathsf{base}):\!\!\equiv\mathsf{N}$ and ${g}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}:=\mathsf{merid}({0_{% \mathbf{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}({1_{\mathbf{2}}})}^{-1}}$. We now show that $f$ and $g$ are quasi-inverses.

First we show by induction that $g(f(x))=x$ for all $x:\Sigma\mathbf{2}$. If $x\equiv\mathsf{N}$, then $g(f(\mathsf{N}))\equiv g(\mathsf{base})\equiv\mathsf{N}$, so we have $\mathsf{refl}_{\mathsf{N}}:g(f(\mathsf{N}))=\mathsf{N}$. If $x\equiv\mathsf{S}$, then $g(f(\mathsf{S}))\equiv g(\mathsf{base})\equiv\mathsf{N}$, and we choose the equality $\mathsf{merid}({1_{\mathbf{2}}}):g(f(\mathsf{S}))=\mathsf{S}$. It remains to show that for any $y:\mathbf{2}$, these equalities are preserved as $x$ varies along $\mathsf{merid}(y)$, which is to say that when $\mathsf{refl}_{\mathsf{N}}$ is transported along $\mathsf{merid}(y)$ it yields $\mathsf{merid}({1_{\mathbf{2}}})$. By transport in path spaces and pulled back fibrations, this means we are to show that

 $\mathord{{{g}\mathopen{}\left({{f}\mathopen{}\left({\mathsf{merid}(y)}\right)% \mathclose{}}\right)\mathclose{}}^{-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\,}}}\mathsf{refl}_{\mathsf{N}}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathsf{merid}(y)=\mathsf{merid}({1_{\mathbf{2}}}).$

Of course, we may cancel $\mathsf{refl}_{\mathsf{N}}$. Now by $\mathbf{2}$-induction, we may assume either $y\equiv{0_{\mathbf{2}}}$ or $y\equiv{1_{\mathbf{2}}}$. If $y\equiv{0_{\mathbf{2}}}$, then we have

 $\displaystyle\mathord{{{g}\mathopen{}\left({{f}\mathopen{}\left({\mathsf{merid% }({0_{\mathbf{2}}})}\right)\mathclose{}}\right)\mathclose{}}^{-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\,}}}\mathsf{% merid}({0_{\mathbf{2}}})$ $\displaystyle=\mathord{{{g}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}% }^{-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\,}}}\mathsf{merid}({0_{\mathbf{2}}})$ $\displaystyle=\mathord{{(\mathsf{merid}({0_{\mathbf{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}({1_{\mathbf{2}}})}^{-1}})}^{-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\,}}}\mathsf{merid}({0_{% \mathbf{2}}})$ $\displaystyle=\mathsf{merid}({1_{\mathbf{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% }({0_{\mathbf{2}}})}^{-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\,}}}\mathsf{merid}({0_{\mathbf{2}}})$ $\displaystyle=\mathsf{merid}({1_{\mathbf{2}}})$

while if $y\equiv{1_{\mathbf{2}}}$, then we have

 $\displaystyle\mathord{{{g}\mathopen{}\left({{f}\mathopen{}\left({\mathsf{merid% }({1_{\mathbf{2}}})}\right)\mathclose{}}\right)\mathclose{}}^{-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\,}}}\mathsf{% merid}({1_{\mathbf{2}}})$ $\displaystyle=\mathord{{{g}\mathopen{}\left({\mathsf{refl}_{\mathsf{base}}}% \right)\mathclose{}}^{-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\,}}}\mathsf{merid}({1_{\mathbf{2}}})$ $\displaystyle=\mathord{{\mathsf{refl}_{\mathsf{N}}}^{-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\,}}}\mathsf{merid}% ({1_{\mathbf{2}}})$ $\displaystyle=\mathsf{merid}({1_{\mathbf{2}}}).$

Thus, for all $x:\Sigma\mathbf{2}$, we have $g(f(x))=x$.

Now we show by induction that $f(g(x))=x$ for all $x:\mathbb{S}^{1}$. If $x\equiv\mathsf{base}$, then $f(g(\mathsf{base}))\equiv f(\mathsf{N})\equiv\mathsf{base}$, so we have $\mathsf{refl}_{\mathsf{base}}:f(g(\mathsf{base}))=\mathsf{base}$. It remains to show that this equality is preserved as $x$ varies along $\mathsf{loop}$, which is to say that it is transported along $\mathsf{loop}$ to itself. Again, by transport in path spaces and pulled back fibrations, this means to show that

 $\mathord{{{f}\mathopen{}\left({{g}\mathopen{}\left({\mathsf{loop}}\right)% \mathclose{}}\right)\mathclose{}}^{-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\,}}}\mathsf{refl}_{\mathsf{base}}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\mathsf{loop}=\mathsf{refl}_{\mathsf{base}}.$

However, we have

 $\displaystyle{f}\mathopen{}\left({{g}\mathopen{}\left({\mathsf{loop}}\right)% \mathclose{}}\right)\mathclose{}$ $\displaystyle={f}\mathopen{}\left({\mathsf{merid}({0_{\mathbf{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}({1_{\mathbf{2}}})}^{-1}}}\right)\mathclose{}$ $\displaystyle={f}\mathopen{}\left({\mathsf{merid}({0_{\mathbf{2}}})}\right)% \mathclose{}\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{{{f}\mathopen{}\left({\mathsf{merid}({1_{\mathbf{2}% }})}\right)\mathclose{}}^{-1}}$ $\displaystyle=\mathsf{loop}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathsf{refl}_{\mathsf{base}}$

so this follows easily. ∎

Topologically, the two-point space $\mathbf{2}$ is also known as the 0-dimensional sphere, $\mathbb{S}^{0}$. (For instance, it is the space of points at distance $1$ from the origin in $\mathbb{R}^{1}$, just as the topological 1-sphere is the space of points at distance $1$ from the origin in $\mathbb{R}^{2}$.) Thus, Lemma 6.5.1 (http://planetmath.org/65suspensions#Thmprelem1) can be phrased suggestively as $\Sigma\mathbb{S}^{0}\simeq\mathbb{S}^{1}$. In fact, this pattern continues: we can define all the spheres inductively by

 $\mathbb{S}^{0}:\!\!\equiv\mathbf{2}\qquad\text{and}\qquad\mathbb{S}^{n+1}:\!\!% \equiv\Sigma\mathbb{S}^{n}.$ (6.5.2)

We can even start one dimension lower by defining $\mathbb{S}^{-1}:\!\!\equiv\mathbf{0}$, and observe that $\Sigma\mathbf{0}\simeq\mathbf{2}$.

To prove carefully that this agrees with the definition of $\mathbb{S}^{n}$ from the previous section would require making the latter more explicit. However, we can show that the recursive definition has the same universal property that we would expect the other one to have. If $(A,a_{0})$ and $(B,b_{0})$ are pointed types (with basepoints often left implicit), let $\mathsf{Map}_{*}(A,B)$ denote the type of based maps:

 $\mathsf{Map}_{*}(A,B):\!\!\equiv\mathchoice{\sum_{f:A\to B}\,}{\mathchoice{{% \textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A% \to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{\sum_{(f:A\to B)}}{\sum_{% (f:A\to B)}}{\sum_{(f:A\to B)}}}{\mathchoice{{\textstyle\sum_{(f:A\to B)}}}{% \sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}{\sum_{(f:A\to B)}}}(f(a_{0})=b_{0}).$

Note that any type $A$ gives rise to a pointed type $A_{+}:\!\!\equiv A+\mathbf{1}$ with basepoint ${\mathsf{inr}}(\star)$; this is called adjoining a disjoint basepoint.

###### Lemma 6.5.3.

For a type $A$ and a pointed type $(B,b_{0})$, we have

 $\mathsf{Map}_{*}(A_{+},B)\simeq(A\to B)$

Note that on the right we have the ordinary type of unbased functions from $A$ to $B$.

###### Proof.

From left to right, given $f:A_{+}\to B$ with $p:f({\mathsf{inr}}(\star))=b_{0}$, we have $f\circ{\mathsf{inl}}:A\to B$. And from right to left, given $g:A\to B$ we define $g^{\prime}:A_{+}\to B$ by $g^{\prime}({\mathsf{inl}}(a)):\!\!\equiv g(a)$ and $g^{\prime}({\mathsf{inr}}(u)):\!\!\equiv b_{0}$. We leave it to the reader to show that these are quasi-inverse operations. ∎

In particular, note that $\mathbf{2}\simeq\mathbf{1}_{+}$. Thus, for any pointed type $B$ we have

 ${\mathsf{Map}_{*}(\mathbf{2},B)}\simeq{(\mathbf{1}\to B)}\simeq B.$

Now recall that the loop space operation $\Omega$ acts on pointed types, with definition $\Omega(A,a_{0}):\!\!\equiv(a_{0}=_{A}a_{0},\mathsf{refl}_{a_{0}})$. We can also make the suspension $\Sigma$ act on pointed types, by $\Sigma(A,a_{0}):\!\!\equiv(\Sigma A,\mathsf{N})$.

###### Lemma 6.5.4.

For pointed types $(A,a_{0})$ and $(B,b_{0})$ we have

 $\mathsf{Map}_{*}(\Sigma A,B)\simeq\mathsf{Map}_{*}(A,\Omega B).$
###### Proof.

From left to right, given $f:\Sigma A\to B$ with $p:f(\mathsf{N})=b_{0}$, we define $g:A\to\Omega B$ by

 $g(a):\!\!\equiv\mathord{{p}^{-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\,}}}{f}\mathopen{}\left({\mathsf{% merid}(a)\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}(a_{0})}^{-1}}}\right)\mathclose{}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}p.$

Then we have

 $\displaystyle g(a_{0})$ $\displaystyle\equiv\mathord{{p}^{-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\,}}}{f}\mathopen{}\left({\mathsf{% merid}(a_{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}(a_{0})}^{-1}}}\right)\mathclose{}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}p$ $\displaystyle=\mathord{{p}^{-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\,}}}{f}\mathopen{}\left({\mathsf{% refl}_{\mathsf{N}}}\right)\mathclose{}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p$ $\displaystyle=\mathord{{p}^{-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\,}}}p$ $\displaystyle=\mathsf{refl}_{b_{0}}.$

Thus, denoting this path by $q:g(a_{0})=\mathsf{refl}_{b_{0}}$, we have $(g,q):\mathsf{Map}_{*}(A,\Omega B)$.

On the other hand, from right to left, given $g:A\to\Omega B$ and $q:g(a_{0})=\mathsf{refl}_{b_{0}}$, we define $f:\Sigma A\to B$ by $\Sigma$-recursion, such that $f(\mathsf{N}):\!\!\equiv b_{0}$ and $f(\mathsf{S}):\!\!\equiv b_{0}$ and

 ${f}\mathopen{}\left({\mathsf{merid}(a)}\right)\mathclose{}:=g(a).$

Then we can simply take $p$ to be $\mathsf{refl}_{b_{0}}:f(\mathsf{N})=b_{0}$.

Now given $(f,p)$, by passing back and forth we obtain $(f^{\prime},p^{\prime})$ where $f^{\prime}$ is defined by $f^{\prime}(\mathsf{N})\equiv b_{0}$ and $f^{\prime}(\mathsf{S})\equiv b_{0}$ and

 ${f^{\prime}}\mathopen{}\left({\mathsf{merid}(a)}\right)\mathclose{}=\mathord{{% p}^{-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\,}}}{f}\mathopen{}\left({\mathsf{merid}(a)\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}(a_{0})}^{-1}}}\right)\mathclose{}\mathchoice{\mathbin{\raisebox% {2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}% }}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p,$

while $p^{\prime}\equiv\mathsf{refl}_{b_{0}}$. To show $f=f^{\prime}$, by function extensionality it suffices to show $f(x)=f^{\prime}(x)$ for all $x:\Sigma A$, so we can use the induction principle of suspension. First, we have

 $f(\mathsf{N})\overset{p}{=}b_{0}\equiv f^{\prime}(\mathsf{N}).$ (6.5.5)

Second, we have

And thirdly, as $x$ varies along $\mathsf{merid}(a)$ we must show that the following diagram of paths commutes (invoking the definition of ${f^{\prime}}\mathopen{}\left({\mathsf{merid}(a)}\right)\mathclose{}$):

This is clear. Thus, to show that $(f,p)=(f^{\prime},p^{\prime})$, it remains only to show that $p$ is identified with $p^{\prime}$ when transported along this equality $f=f^{\prime}$. Since the type of $p$ is $f(\mathsf{N})=b_{0}$, this means essentially that when $p$ is composed on the left with the inverse of the equality (6.5.5), it becomes $p^{\prime}$. But this is obvious, since (6.5.5) is just $p$ itself, while $p^{\prime}$ is reflexivity.

On the other side, suppose given $(g,q)$. By passing back and forth we obtain $(g^{\prime},q^{\prime})$ with

 $\displaystyle g^{\prime}(a)$ $\displaystyle=\mathord{{\mathsf{refl}_{b_{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\,}}}g(a)% \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{{g(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\,}}}\mathsf{refl}_{b_{0}}$ $\displaystyle=g(a)\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{{g(a_{0})}^{-1}}$ $\displaystyle=g(a)$

using $q:g(a_{0})=\mathsf{refl}_{b_{0}}$ in the last equality. Thus, $g^{\prime}=g$ by function extensionality, so it remains to show that when transported along this equality $q$ is identified with $q^{\prime}$. At $a_{0}$, the induced equality $g(a_{0})=g^{\prime}(a_{0})$ consists essentially of $q$ itself, while the definition of $q^{\prime}$ involves only canceling inverses and reflexivities. Thus, some tedious manipulations of naturality finish the proof. ∎

In particular, for the spheres defined as in (6.5.2) we have

 $\mathsf{Map}_{*}(\mathbb{S}^{n},B)\simeq\mathsf{Map}_{*}(\mathbb{S}^{n-1},% \Omega B)\simeq\cdots\simeq\mathsf{Map}_{*}(\mathbf{2},\Omega^{n}B)\simeq% \Omega^{n}B.$

Thus, these spheres $\mathbb{S}^{n}$ have the universal property that we would expect from the spheres defined directly in terms of $n$-fold loop spaces as in §6.4 (http://planetmath.org/64circlesandspheres).

Title 6.5 Suspensions
\metatable