6.4 Circles and spheres

We have already discussed the circle π•Š1 as the higher inductive type generated by

  • β€’

    A point π–»π–Ίπ—Œπ–Ύ:π•Š1, and

  • β€’

    A path π—…π—ˆπ—ˆπ—‰:π–»π–Ίπ—Œπ–Ύ=π•Š1π–»π–Ίπ—Œπ–Ύ.

Its inductionMathworldPlanetmath principle says that given P:π•Š1→𝒰 along with b:P⁒(π–»π–Ίπ—Œπ–Ύ) and β„“:b=π—…π—ˆπ—ˆπ—‰Pb, we have f:∏(x:π•Š1)P⁒(x) with f⁒(π–»π–Ίπ—Œπ–Ύ)≑b and 𝖺𝗉𝖽f(π—…π—ˆπ—ˆπ—‰)=β„“. Its non-dependent recursion principle says that given B with b:B and β„“:b=b, we have f:π•Š1β†’B with f⁒(π–»π–Ίπ—Œπ–Ύ)≑b and f(π—…π—ˆπ—ˆπ—‰)=β„“.

We observe that the circle is nontrivial.

Lemma 6.4.1.

π—…π—ˆπ—ˆπ—‰β‰ π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ.


Suppose that π—…π—ˆπ—ˆπ—‰=π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ. Then since for any type A with x:A and p:x=x, there is a function f:π•Š1β†’A defined by f(π–»π–Ίπ—Œπ–Ύ):≑x and f(π—…π—ˆπ—ˆπ—‰):=p, we have


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 ∏(x:S1)(x=x) which is not equal to x↦reflx.


We define f:∏(x:π•Š1)(x=x) by π•Š1-induction. When x is π–»π–Ίπ—Œπ–Ύ, we let f(π–»π–Ίπ—Œπ–Ύ):β‰‘π—…π—ˆπ—ˆπ—‰. Now when x varies along π—…π—ˆπ—ˆπ—‰ (see Remark 6.2.4 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprermk3)), we must show that π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦x=x⁒(π—…π—ˆπ—ˆπ—‰,π—…π—ˆπ—ˆπ—‰)=π—…π—ˆπ—ˆπ—‰. However, in Β§2.11 (http://planetmath.org/211identitytype) we observed that π—π—‹π–Ίπ—‡π—Œπ—‰π—ˆπ—‹π—x↦x=x⁒(p,q)=p-1⁒\centerdot⁒q⁒\centerdot⁒p, so what we have to show is that π—…π—ˆπ—ˆπ—‰-1⁒\centerdotβ’π—…π—ˆπ—ˆπ—‰β’\centerdotβ’π—…π—ˆπ—ˆπ—‰=π—…π—ˆπ—ˆπ—‰. But this is clear by canceling an inverseMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath.

To show that fβ‰ (x↦𝗋𝖾𝖿𝗅x), it suffices by function extensionality to show that f⁒(π–»π–Ίπ—Œπ–Ύ)β‰ π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ. But f⁒(π–»π–Ίπ—Œπ–Ύ)=π—…π—ˆπ—ˆπ—‰, 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 universePlanetmathPlanetmath which contains the circle cannot be a 1-type.

Corollary 6.4.3.

If the type S1 belongs to some universe U, then U is not a 1-type.


The type π•Š1=π•Š1 in 𝒰 is, by univalence, equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to the type π•Š1β‰ƒπ•Š1 of autoequivalences of π•Š1, so it suffices to show that π•Š1β‰ƒπ•Š1 is not a set. For this, it suffices to show that its equality type π—‚π–½π•Š1=(π•Š1β‰ƒπ•Š1)π—‚π–½π•Š1 is not a mere proposition. Since being an equivalence is a mere proposition, this type is equivalent to π—‚π–½π•Š1=(π•Š1β†’π•Š1)π—‚π–½π•Š1. But by function extensionality, this is equivalent to ∏(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 π–»π–Ίπ—Œπ–Ύ:π•Š2, and

  • β€’

    A 2-dimensional path π—Œπ—Žπ—‹π–Ώ:π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ=π—‹π–Ύπ–Ώπ—…π–»π–Ίπ—Œπ–Ύ in π–»π–Ίπ—Œπ–Ύ=π–»π–Ίπ—Œπ–Ύ.

The recursion principle for π•Š2 is not hard: it says that given B with b:B and s:𝗋𝖾𝖿𝗅b=𝗋𝖾𝖿𝗅b, we have f:π•Š2β†’B with f⁒(π–»π–Ίπ—Œπ–Ύ)≑b and 𝖺𝗉f2(π—Œπ—Žπ—‹π–Ώ)=s. Here by β€œπ–Ίπ—‰f2(π—Œπ—Žπ—‹π–Ώ)” we mean an extensionPlanetmathPlanetmathPlanetmath of the functorial action of f to two-dimensional paths, which can be stated precisely as follows.

Lemma 6.4.4.

Given f:A→B and x,y:A and p,q:x=y, and r:p=q, we have a path apf2(r):f(p)=f(q).


By path induction, we may assume p≑q and r is reflexivityMathworldPlanetmath. But then we may define 𝖺𝗉f2(𝗋𝖾𝖿𝗅p):≑𝗋𝖾𝖿𝗅f(p). ∎

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β†’U and x,y:A and p,q:x=y and r:p=q, for any u:P⁒(x) we have transport2(r,u):p*(u)=q*(u).


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=pPv and k:u=qPv. By our definition of dependent paths, this means h:p*(u)=v and k:q*(u)=v. Thus, it is reasonable to define the type of dependent 2-paths over r to be


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

Lemma 6.4.6.

Given P:Aβ†’U and x,y:A and p,q:x=y and r:p=q and a function f:∏(x:A)P⁒(x), we have apdf2(r):apdf(p)=rPapdf(q).


Path induction. ∎

Now we can state the induction principle for π•Š2: given P:π•Š2β†’P with b:P⁒(π–»π–Ίπ—Œπ–Ύ) and s:𝗋𝖾𝖿𝗅b=π—Œπ—Žπ—‹π–ΏP𝗋𝖾𝖿𝗅b, there is a function f:∏(x:π•Š2)P⁒(x) such that f⁒(π–»π–Ίπ—Œπ–Ύ)≑b and 𝖺𝗉𝖽f2(π—Œπ—Žπ—‹π–Ώ)=s.

Of course, this explicit approach gets more and more complicated as we go up in dimensionMathworldPlanetmath. 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 spaceMathworldPlanetmath Ξ©n:𝒰*→𝒰* (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 π–»π–Ίπ—Œπ–Ύ:π•Šn, and

  • β€’

    An n-loop π—…π—ˆπ—ˆπ—‰n:Ξ©n⁒(π•Šn,π–»π–Ίπ—Œπ–Ύ).

In order to write down the induction principle for this presentationMathworldPlanetmathPlanetmathPlanetmath, 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 sectionPlanetmathPlanetmathPlanetmath we will discuss a different way to define the spheres that is sometimes more tractable.

Title 6.4 Circles and spheres