# 6.4 Circles and spheres

We have already discussed the circle $\mathbb{S}^{1}$ as the higher inductive type generated by

• A point $\mathsf{base}:\mathbb{S}^{1}$, and

• A path $\mathsf{loop}:{\mathsf{base}=_{\mathbb{S}^{1}}\mathsf{base}}$.

Its induction principle says that given $P:\mathbb{S}^{1}\to\mathcal{U}$ along with $b:P(\mathsf{base})$ and $\ell:b=^{P}_{\mathsf{loop}}b$, we have $f:\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}P(x)$ with $f(\mathsf{base})\equiv b$ and $\mathsf{apd}_{f}\mathopen{}\left(\mathsf{loop}\right)\mathclose{}=\ell$. Its non-dependent recursion principle says that given $B$ with $b:B$ and $\ell:b=b$, we have $f:\mathbb{S}^{1}\to B$ with $f(\mathsf{base})\equiv b$ and ${f}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}=\ell$.

We observe that the circle is nontrivial.

###### Lemma 6.4.1.

$\mathsf{loop}\neq\mathsf{refl}_{\mathsf{base}}$.

###### Proof.

Suppose that $\mathsf{loop}=\mathsf{refl}_{\mathsf{base}}$. Then since for any type $A$ with $x:A$ and $p:x=x$, there is a function $f:\mathbb{S}^{1}\to A$ defined by $f(\mathsf{base}):\!\!\equiv x$ and ${f}\mathopen{}\left({\mathsf{loop}}\right)\mathclose{}:=p$, we have

 $p=f(\mathsf{loop})=f(\mathsf{refl}_{\mathsf{base}})=\mathsf{refl}_{x}.$

But this implies that every type is a set, which as we have seen is not the case (see Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6)). ∎

The circle also has the following interesting property, which is useful as a source of counterexamples.

###### Lemma 6.4.2.

There exists an element of $\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}(x=x)$ which is not equal to $x\mapsto\mathsf{refl}_{x}$.

###### Proof.

We define $f:\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}(x=x)$ by $\mathbb{S}^{1}$-induction. When $x$ is $\mathsf{base}$, we let $f(\mathsf{base}):\!\!\equiv\mathsf{loop}$. Now when $x$ varies along $\mathsf{loop}$ (see Remark 6.2.4 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprermk3)), we must show that $\mathsf{transport}^{x\mapsto x=x}(\mathsf{loop},\mathsf{loop})=\mathsf{loop}$. However, in §2.11 (http://planetmath.org/211identitytype) we observed that $\mathsf{transport}^{x\mapsto x=x}(p,q)=\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\,}}}q\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\,}}}p$, so what we have to show is that $\mathord{{\mathsf{loop}}^{-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{loop}\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{% loop}=\mathsf{loop}$. But this is clear by canceling an inverse.

To show that $f\neq(x\mapsto\mathsf{refl}_{x})$, it suffices by function extensionality to show that $f(\mathsf{base})\neq\mathsf{refl}_{\mathsf{base}}$. But $f(\mathsf{base})=\mathsf{loop}$, so this is just the previous lemma. ∎

For instance, this enables us to extend Example 3.1.9 (http://planetmath.org/31setsandntypes#Thmpreeg6) by showing that any universe which contains the circle cannot be a 1-type.

###### Corollary 6.4.3.

If the type $\mathbb{S}^{1}$ belongs to some universe $\mathcal{U}$, then $\mathcal{U}$ is not a 1-type.

###### Proof.

The type $\mathbb{S}^{1}=\mathbb{S}^{1}$ in $\mathcal{U}$ is, by univalence, equivalent to the type $\mathbb{S}^{1}\simeq\mathbb{S}^{1}$ of autoequivalences of $\mathbb{S}^{1}$, so it suffices to show that $\mathbb{S}^{1}\simeq\mathbb{S}^{1}$ is not a set. For this, it suffices to show that its equality type $\mathsf{id}_{\mathbb{S}^{1}}=_{(\mathbb{S}^{1}\simeq\mathbb{S}^{1})}\mathsf{id% }_{\mathbb{S}^{1}}$ is not a mere proposition. Since being an equivalence is a mere proposition, this type is equivalent to $\mathsf{id}_{\mathbb{S}^{1}}=_{(\mathbb{S}^{1}\to\mathbb{S}^{1})}\mathsf{id}_{% \mathbb{S}^{1}}$. But by function extensionality, this is equivalent to $\mathchoice{\prod_{x:\mathbb{S}^{1}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{1})}}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{% \prod_{(x:\mathbb{S}^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}% }}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S% }^{1})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{1})}}}{\prod_{(x:% \mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}{\prod_{(x:\mathbb{S}^{1})}}}(x=x)$, which as we have seen in Lemma 6.4.2 (http://planetmath.org/64circlesandspheres#Thmprelem2) contains two unequal elements. ∎

We have also mentioned that the 2-sphere $\mathbb{S}^{2}$ should be the higher inductive type generated by

• A point $\mathsf{base}:\mathbb{S}^{2}$, and

• A 2-dimensional path $\mathsf{surf}:\mathsf{refl}_{\mathsf{base}}=\mathsf{refl}_{\mathsf{base}}$ in ${\mathsf{base}=\mathsf{base}}$.

The recursion principle for $\mathbb{S}^{2}$ is not hard: it says that given $B$ with $b:B$ and $s:\mathsf{refl}_{b}=\mathsf{refl}_{b}$, we have $f:\mathbb{S}^{2}\to B$ with $f(\mathsf{base})\equiv b$ and $\mathsf{ap}^{2}_{f}\mathopen{}\left({\mathsf{surf}}\right)\mathclose{}=s$. Here by “$\mathsf{ap}^{2}_{f}\mathopen{}\left({\mathsf{surf}}\right)\mathclose{}$” we mean an extension of the functorial action of $f$ to two-dimensional paths, which can be stated precisely as follows.

###### Lemma 6.4.4.

Given $f:A\to B$ and $x,y:A$ and $p,q:x=y$, and $r:p=q$, we have a path $\mathsf{ap}^{2}_{f}\mathopen{}\left({r}\right)\mathclose{}:{f}\mathopen{}\left% ({p}\right)\mathclose{}={f}\mathopen{}\left({q}\right)\mathclose{}$.

###### Proof.

By path induction, we may assume $p\equiv q$ and $r$ is reflexivity. But then we may define $\mathsf{ap}^{2}_{f}\mathopen{}\left({\mathsf{refl}_{p}}\right)\mathclose{}:\!% \!\equiv\mathsf{refl}_{{f}\mathopen{}\left({p}\right)\mathclose{}}$. ∎

In order to state the general induction principle, we need a version of this lemma for dependent functions, which in turn requires a notion of dependent two-dimensional paths. As before, there are many ways to define such a thing; one is by way of a two-dimensional version of transport.

###### Lemma 6.4.5.

Given $P:A\to\mathcal{U}$ and $x,y:A$ and $p,q:x=y$ and $r:p=q$, for any $u:P(x)$ we have $\mathsf{transport}^{2}\mathopen{}\left({r},{u}\right)\mathclose{}:{p}_{*}% \mathopen{}\left({u}\right)\mathclose{}={q}_{*}\mathopen{}\left({u}\right)% \mathclose{}$.

###### Proof.

By path induction. ∎

Now suppose given $x,y:A$ and $p,q:x=y$ and $r:p=q$ and also points $u:P(x)$ and $v:P(y)$ and dependent paths $h:u=^{P}_{p}v$ and $k:u=^{P}_{q}v$. By our definition of dependent paths, this means $h:{p}_{*}\mathopen{}\left({u}\right)\mathclose{}=v$ and $k:{q}_{*}\mathopen{}\left({u}\right)\mathclose{}=v$. Thus, it is reasonable to define the type of dependent 2-paths over $r$ to be

 $(h=^{P}_{r}k):\!\!\equiv(h=\mathsf{transport}^{2}\mathopen{}\left({r},{u}% \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\,}}}k).$

We can now state the dependent version of Lemma 6.4.4 (http://planetmath.org/64circlesandspheres#Thmprelem3).

###### Lemma 6.4.6.

Given $P:A\to\mathcal{U}$ and $x,y:A$ and $p,q:x=y$ and $r:p=q$ and a function $f:\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)}}}P(x)$, we have $\mathsf{apd}^{2}_{f}\mathopen{}\left(r\right)\mathclose{}:\mathsf{apd}_{f}% \mathopen{}\left(p\right)\mathclose{}=^{P}_{r}\mathsf{apd}_{f}\mathopen{}\left% (q\right)\mathclose{}$.

###### Proof.

Path induction. ∎

Now we can state the induction principle for $\mathbb{S}^{2}$: given $P:\mathbb{S}^{2}\to P$ with $b:P(\mathsf{base})$ and $s:\mathsf{refl}_{b}=^{P}_{\mathsf{surf}}\mathsf{refl}_{b}$, there is a function $f:\mathchoice{\prod_{x:\mathbb{S}^{2}}\,}{\mathchoice{{\textstyle\prod_{(x:% \mathbb{S}^{2})}}}{\prod_{(x:\mathbb{S}^{2})}}{\prod_{(x:\mathbb{S}^{2})}}{% \prod_{(x:\mathbb{S}^{2})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{2})}% }}{\prod_{(x:\mathbb{S}^{2})}}{\prod_{(x:\mathbb{S}^{2})}}{\prod_{(x:\mathbb{S% }^{2})}}}{\mathchoice{{\textstyle\prod_{(x:\mathbb{S}^{2})}}}{\prod_{(x:% \mathbb{S}^{2})}}{\prod_{(x:\mathbb{S}^{2})}}{\prod_{(x:\mathbb{S}^{2})}}}P(x)$ such that $f(\mathsf{base})\equiv b$ and $\mathsf{apd}^{2}_{f}\mathopen{}\left(\mathsf{surf}\right)\mathclose{}=s$.

Of course, this explicit approach gets more and more complicated as we go up in dimension. Thus, if we want to define $n$-spheres for all $n$, we need some more systematic idea. One approach is to work with $n$-dimensional loops directly, rather than general $n$-dimensional paths.

Recall from §2.1 (http://planetmath.org/21typesarehighergroupoids) the definitions of pointed types $\mathcal{U}_{*}$, and the $n$-fold loop space $\Omega^{n}:\mathcal{U}_{*}\to\mathcal{U}_{*}$ (Definition 2.1.7 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn1) and Definition 2.1.8 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn2)). Now we can define the $n$-sphere $\mathbb{S}^{n}$ to be the higher inductive type generated by

• A point $\mathsf{base}:\mathbb{S}^{n}$, and

• An $n$-loop $\mathsf{loop}_{n}:\Omega^{n}(\mathbb{S}^{n},\mathsf{base})$.

In order to write down the induction principle for this presentation, we would need to define a notion of “dependent $n$-loop”, along with the action of dependent functions on $n$-loops. We leave this to the reader (see http://planetmath.org/node/87769Exercise 6.4); in the next section we will discuss a different way to define the spheres that is sometimes more tractable.

Title 6.4 Circles and spheres
\metatable