6.4 Circles and spheres

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

• A point $\mathrm{𝖻𝖺𝗌𝖾}:{𝕊}^1$, and

• A path $\mathrm{𝗅𝗈𝗈𝗉}:\mathrm{𝖻𝖺𝗌𝖾}{=}_{{𝕊}^1}\mathrm{𝖻𝖺𝗌𝖾}$.

Its induction principle says that given $P:{𝕊}^1\to 𝒰$ along with $b:P(\mathrm{𝖻𝖺𝗌𝖾})$ and $\mathrm{\ell }:b{=}_{\mathrm{𝗅𝗈𝗈𝗉}}^{P}b$, we have $f:{\prod }_{(x:{𝕊}^1)}P(x)$ with $f(\mathrm{𝖻𝖺𝗌𝖾})\equiv b$ and ${\mathrm{𝖺𝗉𝖽}}_f\left(\mathrm{𝗅𝗈𝗈𝗉}\right)=\mathrm{\ell }$.Its non-dependent recursion principle says that given $B$ with $b:B$ and $\mathrm{\ell }:b=b$, we have $f:{𝕊}^1\to B$ with $f(\mathrm{𝖻𝖺𝗌𝖾})\equiv b$ and $f\left(\mathrm{𝗅𝗈𝗈𝗉}\right)=\mathrm{\ell }$.

We observe that the circle is nontrivial.

Lemma 6.4.1.

$\mathrm{𝗅𝗈𝗈𝗉}\ne {\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$.

Proof.

Suppose that $\mathrm{𝗅𝗈𝗈𝗉}={\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$.Then since for any type $A$ with $x:A$ and $p:x=x$, there is a function $f:{𝕊}^1\to A$ defined by $f(\mathrm{𝖻𝖺𝗌𝖾}):\equiv x$ and $f\left(\mathrm{𝗅𝗈𝗈𝗉}\right):=p$, we have

$$p=f(\mathrm{𝗅𝗈𝗈𝗉})=f({\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}})={\mathrm{𝗋𝖾𝖿𝗅}}_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 ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}{\mathrm{S}}^{\mathrm{1}}\mathrm{)}}\mathrm{(}x\mathrm{=}x\mathrm{)}$ which is not equal to $x\mathrm{\mapsto }{\mathrm{refl}}_x$.

Proof.

We define $f:{\prod }_{(x:{𝕊}^1)}(x=x)$ by ${𝕊}^1$-induction.When $x$ is $\mathrm{𝖻𝖺𝗌𝖾}$, we let $f(\mathrm{𝖻𝖺𝗌𝖾}):\equiv \mathrm{𝗅𝗈𝗈𝗉}$.Now when $x$ varies along $\mathrm{𝗅𝗈𝗈𝗉}$ (see Remark 6.2.4 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprermk3)), we must show that ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto x=x}(\mathrm{𝗅𝗈𝗈𝗉},\mathrm{𝗅𝗈𝗈𝗉})=\mathrm{𝗅𝗈𝗈𝗉}$.However, in §2.11 (http://planetmath.org/211identitytype) we observed that ${\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^{x\mapsto x=x}(p,q)=p^{-1}qp$, so what we have to show is that ${\mathrm{𝗅𝗈𝗈𝗉}}^{-1}\mathrm{𝗅𝗈𝗈𝗉}\mathrm{𝗅𝗈𝗈𝗉}=\mathrm{𝗅𝗈𝗈𝗉}$.But this is clear by canceling an inverse.

To show that $f\ne (x\mapsto {\mathrm{𝗋𝖾𝖿𝗅}}_x)$, it suffices by function extensionality to show that $f(\mathrm{𝖻𝖺𝗌𝖾})\ne {\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$.But $f(\mathrm{𝖻𝖺𝗌𝖾})=\mathrm{𝗅𝗈𝗈𝗉}$, 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 ${\mathrm{S}}^{\mathrm{1}}$ belongs to some universe $\mathrm{U}$, then $\mathrm{U}$ is not a 1-type.

Proof.

The type ${𝕊}^1={𝕊}^1$ in $𝒰$ is, by univalence, equivalent to the type ${𝕊}^1\simeq {𝕊}^1$ of autoequivalences of ${𝕊}^1$, so it suffices to show that ${𝕊}^1\simeq {𝕊}^1$ is not a set.For this, it suffices to show that its equality type ${\mathrm{𝗂𝖽}}_{{𝕊}^1}{=}_{({𝕊}^1\simeq {𝕊}^1)}{\mathrm{𝗂𝖽}}_{{𝕊}^1}$ is not a mere proposition.Since being an equivalence is a mere proposition, this type is equivalent to ${\mathrm{𝗂𝖽}}_{{𝕊}^1}{=}_{({𝕊}^1\to {𝕊}^1)}{\mathrm{𝗂𝖽}}_{{𝕊}^1}$.But by function extensionality, this is equivalent to ${\prod }_{(x:{𝕊}^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 ${𝕊}^2$ should be the higher inductive type generated by

• A point $\mathrm{𝖻𝖺𝗌𝖾}:{𝕊}^2$, and

• A 2-dimensional path $\mathrm{𝗌𝗎𝗋𝖿}:{\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}={\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝖻𝖺𝗌𝖾}}$ in $\mathrm{𝖻𝖺𝗌𝖾}=\mathrm{𝖻𝖺𝗌𝖾}$.

The recursion principle for ${𝕊}^2$ is not hard: it says that given $B$ with $b:B$ and $s:{\mathrm{𝗋𝖾𝖿𝗅}}_b={\mathrm{𝗋𝖾𝖿𝗅}}_b$, we have $f:{𝕊}^2\to B$ with $f(\mathrm{𝖻𝖺𝗌𝖾})\equiv b$ and ${\mathrm{𝖺𝗉}}_f^2\left(\mathrm{𝗌𝗎𝗋𝖿}\right)=s$.Here by “${\mathrm{𝖺𝗉}}_f^2\left(\mathrm{𝗌𝗎𝗋𝖿}\right)$” 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\mathrm{:}A\mathrm{\to }B$ and $x\mathrm{,}y\mathrm{:}A$ and $p\mathrm{,}q\mathrm{:}x\mathrm{=}y$, and $r\mathrm{:}p\mathrm{=}q$, we have a path ${\mathrm{ap}}_f^{\mathrm{2}}\mathrm{\left(}r\mathrm{\right)}\mathrm{:}f\mathrm{\left(}p\mathrm{\right)}\mathrm{=}f\mathrm{\left(}q\mathrm{\right)}$.

Proof.

By path induction, we may assume $p\equiv q$ and $r$ is reflexivity.But then we may define ${\mathrm{𝖺𝗉}}_f^2\left({\mathrm{𝗋𝖾𝖿𝗅}}_p\right):\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{f\left(p\right)}$.∎

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\mathrm{:}A\mathrm{\to }\mathrm{U}$ and $x\mathrm{,}y\mathrm{:}A$ and $p\mathrm{,}q\mathrm{:}x\mathrm{=}y$ and $r\mathrm{:}p\mathrm{=}q$, for any $u\mathrm{:}P\mathit{}\mathrm{(}x\mathrm{)}$ we have ${\mathrm{transport}}^{\mathrm{2}}\mathrm{(}r\mathrm{,}u\mathrm{)}\mathrm{:}{p}_{\mathrm{*}}\mathrm{\left(}u\mathrm{\right)}\mathrm{=}{q}_{\mathrm{*}}\mathrm{\left(}u\mathrm{\right)}$.

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{=}_q^{P}v$.By our definition of dependent paths, this means $h:p_{*}\left(u\right)=v$ and $k:q_{*}\left(u\right)=v$.Thus, it is reasonable to define the type of dependent 2-paths over $r$ to be

$$(h{=}_r^{P}k):\equiv (h={\mathrm{𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍}}^2(r,u)k).$$

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

Lemma 6.4.6.

Given $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ and $x\mathrm{,}y\mathrm{:}A$ and $p\mathrm{,}q\mathrm{:}x\mathrm{=}y$ and $r\mathrm{:}p\mathrm{=}q$ and a function $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$, we have${\mathrm{apd}}_f^{\mathrm{2}}\mathrm{\left(}r\mathrm{\right)}\mathrm{:}{\mathrm{apd}}_f\mathrm{\left(}p\mathrm{\right)}{\mathrm{=}}_r^P{\mathrm{apd}}_f\mathrm{\left(}q\mathrm{\right)}$.

Proof.

Path induction.∎

Now we can state the induction principle for ${𝕊}^2$: given $P:{𝕊}^2\to P$ with $b:P(\mathrm{𝖻𝖺𝗌𝖾})$ and $s:{\mathrm{𝗋𝖾𝖿𝗅}}_b{=}_{\mathrm{𝗌𝗎𝗋𝖿}}^P{\mathrm{𝗋𝖾𝖿𝗅}}_b$, there is a function $f:{\prod }_{(x:{𝕊}^2)}P(x)$ such that $f(\mathrm{𝖻𝖺𝗌𝖾})\equiv b$ and ${\mathrm{𝖺𝗉𝖽}}_f^2\left(\mathrm{𝗌𝗎𝗋𝖿}\right)=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 ${𝒰}_{*}$, and the $n$-fold loop space ${\mathrm{\Omega }}^n:{𝒰}_{*}\to {𝒰}_{*}$(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 ${𝕊}^n$ to be the higher inductive type generated by

• A point $\mathrm{𝖻𝖺𝗌𝖾}:{𝕊}^n$, and

• An $n$-loop ${\mathrm{𝗅𝗈𝗈𝗉}}_n:{\mathrm{\Omega }}^n({𝕊}^n,\mathrm{𝖻𝖺𝗌𝖾})$.

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.