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