6.4 Circles and spheres
We have already discussed the circle as the higher inductive type generated by
A point , and
A path .
We observe that the circle is nontrivial.
Suppose that . Then since for any type with and , there is a function defined by and , 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.
There exists an element of which is not equal to .
We define by -induction. When is , we let . Now when varies along (see Remark 6.2.4 (http://planetmath.org/62inductionprinciplesanddependentpaths#Thmprermk3)), we must show that . However, in §2.11 (http://planetmath.org/211identitytype) we observed that , so what we have to show is that . But this is clear by canceling an inverse.
To show that , it suffices by function extensionality to show that . But , so this is just the previous lemma. ∎
If the type belongs to some universe , then is not a 1-type.
The type in is, by univalence, equivalent to the type of autoequivalences of , so it suffices to show that is not a set. For this, it suffices to show that its equality type is not a mere proposition. Since being an equivalence is a mere proposition, this type is equivalent to . But by function extensionality, this is equivalent to , 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 should be the higher inductive type generated by
A point , and
A 2-dimensional path in .
The recursion principle for is not hard: it says that given with and , we have with and . Here by “” we mean an extension of the functorial action of to two-dimensional paths, which can be stated precisely as follows.
Given and and , and , we have a path .
By path induction, we may assume and is reflexivity. But then we may define . ∎
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.
Given and and and , for any we have .
By path induction. ∎
Now suppose given and and and also points and and dependent paths and . By our definition of dependent paths, this means and . Thus, it is reasonable to define the type of dependent 2-paths over to be
We can now state the dependent version of Lemma 6.4.4 (http://planetmath.org/64circlesandspheres#Thmprelem3).
Given and and and and a function , we have .
Path induction. ∎
Now we can state the induction principle for : given with and , there is a function such that and .
Of course, this explicit approach gets more and more complicated as we go up in dimension. Thus, if we want to define -spheres for all , we need some more systematic idea. One approach is to work with -dimensional loops directly, rather than general -dimensional paths.
Recall from §2.1 (http://planetmath.org/21typesarehighergroupoids) the definitions of pointed types , and the -fold loop space (Definition 2.1.7 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn1) and Definition 2.1.8 (http://planetmath.org/21typesarehighergroupoids#Thmpredefn2)). Now we can define the -sphere to be the higher inductive type generated by
A point , and
An -loop .
In order to write down the induction principle for this presentation, we would need to define a notion of “dependent -loop”, along with the action of dependent functions on -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|