The suspension of a type is the universal way of making the points of into paths (and hence the paths in into 2-paths, and so on). It is a type defined by the following generators:11There is an unfortunate clash of notation with dependent pair types, which of course are also written with a . However, context usually disambiguates.
a point ,
a point , and
a function .
The names are intended to suggest a “globe” of sorts, with a north pole, a south pole, and an ’s worth of meridians from one to the other. Indeed, as we will see, if , then its suspension is equivalent to the surface of an ordinary sphere, .
The recursion principle for says that given a type together with
a function ,
we have a function such that and , and for all we have . Similarly, the induction principle says that given together with
a point ,
a point , and
for each , a path ,
there exists a function such that and and for each we have .
Our first observation about suspension is that it gives another way to define the circle.
Define by recursion such that and , while but . Define by recursion such that and . We now show that and are quasi-inverses.
First we show by induction that for all . If , then , so we have . If , then , and we choose the equality . It remains to show that for any , these equalities are preserved as varies along , which is to say that when is transported along it yields . By transport in path spaces and pulled back fibrations, this means we are to show that
Of course, we may cancel . Now by -induction, we may assume either or . If , then we have
while if , then we have
Thus, for all , we have .
Now we show by induction that for all . If , then , so we have . It remains to show that this equality is preserved as varies along , which is to say that it is transported along to itself. Again, by transport in path spaces and pulled back fibrations, this means to show that
However, we have
so this follows easily. ∎
Topologically, the two-point space is also known as the 0-dimensional sphere, . (For instance, it is the space of points at distance from the origin in , just as the topological 1-sphere is the space of points at distance from the origin in .) Thus, Lemma 6.5.1 (http://planetmath.org/65suspensions#Thmprelem1) can be phrased suggestively as . In fact, this pattern continues: we can define all the spheres inductively by
We can even start one dimension lower by defining , and observe that .
To prove carefully that this agrees with the definition of from the previous section would require making the latter more explicit. However, we can show that the recursive definition has the same universal property that we would expect the other one to have. If and are pointed types (with basepoints often left implicit), let denote the type of based maps:
Note that any type gives rise to a pointed type with basepoint ; this is called adjoining a disjoint basepoint.
For a type and a pointed type , we have
Note that on the right we have the ordinary type of unbased functions from to .
From left to right, given with , we have . And from right to left, given we define by and . We leave it to the reader to show that these are quasi-inverse operations. ∎
In particular, note that . Thus, for any pointed type we have
Now recall that the loop space operation acts on pointed types, with definition . We can also make the suspension act on pointed types, by .
For pointed types and we have
From left to right, given with , we define by
Then we have
Thus, denoting this path by , we have .
On the other hand, from right to left, given and , we define by -recursion, such that and and
Then we can simply take to be .
Now given , by passing back and forth we obtain where is defined by and and
while . To show , by function extensionality it suffices to show for all , so we can use the induction principle of suspension. First, we have
Second, we have
And thirdly, as varies along we must show that the following diagram of paths commutes (invoking the definition of ):
This is clear. Thus, to show that , it remains only to show that is identified with when transported along this equality . Since the type of is , this means essentially that when is composed on the left with the inverse of the equality (6.5.5), it becomes . But this is obvious, since (6.5.5) is just itself, while is reflexivity.
On the other side, suppose given . By passing back and forth we obtain with
using in the last equality. Thus, by function extensionality, so it remains to show that when transported along this equality is identified with . At , the induced equality consists essentially of itself, while the definition of involves only canceling inverses and reflexivities. Thus, some tedious manipulations of naturality finish the proof. ∎
In particular, for the spheres defined as in (6.5.2) we have
Thus, these spheres have the universal property that we would expect from the spheres defined directly in terms of -fold loop spaces as in §6.4 (http://planetmath.org/64circlesandspheres).