The loop space of the 2-sphere

Back in January 2016 I gave an introductory talk at the University of Ljubljana about Homotopy Type Theory. The goal of this talk was to display some basic techniques in the field, such as constructing higher inductive types, and using the encode-decode method to figure out what its identity type is.


Recall that the topological space \mathbb{S}^2 can be described either as the set of unit vectors of \mathbb{R}^3, or equivalently as the suspension of \mathbb{S}^1. Likewise, \mathbb{S}^{n+1} can be described as the suspension of \mathbb{S}^n. Topologists study spaces by studying their homotopy groups. This turns out to be an intensely hard problem even for simple spaces like the spheres. An approach we like to take for the purpose of this lecture is to study a space by studying its actual loop space. More precisely, we want to present the loop space of the spheres as the universal space with some data.

We will restrict our attention to the 2-sphere, since that is the first sphere which has infinitely non-zero homotopy groups.

For any space X we may consider the fibration \mathrm{hom}(\mathbb{S}^1,X) \twoheadrightarrow X of free loops in X. The loop space of the sphere turns out to be the (homotopy) initial triple (X, x_0, h) consisting of a space X with a base point x_0 and a section of the free loops fibration. Homotopy type theory provides the right tools to consider spaces with such description without complication, via a construction called higher inductive types.

A higher inductive type is a type X which is described by specifying points and paths in the same way an algebra might be specified by generators and relations. For instance, the circle is a type with

\mathsf{base} : \mathbb{S}^1
\mathsf{loop} : \mathsf{base} =_{\mathbb{S}^1} \mathsf{base}.

It turns out that paths have many things in common with equality. For instance, the path fibration P_X \twoheadrightarrow X\times X is the homotopy initial reflexive fibration (i.e. with a map X \to P_X mapping into the diagonal), just as the equality is the least reflexive relation. About the only thing that requires getting used to is that the space of paths with fixed endpoints might actually be interesting. The situation where the `object’ of equalities might be interesting does not occur immediately in set-based mathematics, but it is something which category theorists have been used to for a long time. Since paths and equality have so much in common, we use the equality symbol for the `path type’ or `identity type’.

The circle is not just any type with these elements, but it is the initial such type. The way we express this in type theory is via an inductive principle, which bears similarities with the inductive principle for the natural numbers, and it reads much like a universal property. The inductive principle for \mathbb{S}^1 says that to find a section of a fibration
P \twoheadrightarrow \mathbb{S}^1, we must find a point x : P (\mathsf{base}) above the base point, and show that the other endpoint of the lift at x of \mathsf{loop} matches with x. In type theory, we say this as follows:

x : P (\mathsf{base})
p : \mathsf{trans} (\mathsf{loop}, x) =_{P(\mathsf{base})} x

To construct interesting type families, we therefore need interesting paths in the universe. This is where the univalence axiom comes in. The univalence axiom asserts that the canonical map of type (A =_{U} B) \to (A \simeq B) from equalities between types to equivalences between types, is itself an equivalence. For instance, with the univalence axiom, we can construct a type family over \mathbb{S}^1 by specifying

\mathbb{Z} : U
\mathsf{succ} : \mathbb{Z} \simeq \mathbb{Z}

This type family encodes how many times a loop goes around counterclockwise. The method of proof that this type family is equivalent to the type family x \mapsto (x =_{\mathbb{S}^1} \mathsf{base}) is called the encode-decode method. It is directly analogous to the traditional way of showing that we have a universal cover. The encode-decode method is based on the idea that, to show that a cover C:A\to{} U with r : C (x_0) is equivalent to paths to x_0, it suffices to show that the total space of C is contractible, with center of contraction (x_0, r). To show that the total space of C is contractible, we have to find a term of type

\Pi_{(x:A)}\Pi_{(y:C(x))}~(x_0, r) = (x, y).

The type of identifications (x_0, r) = (x, y) is equivalent to the type \Sigma_{(p:x_0=x)}\ \mathsf{trans}(p, r) = y. Thus, we have the following theorem.

Theorem (encode-decode method).
Let A be a type with a base point x_0. Let C : A \to{} U be a type family over A with r : C(x_0). If we have a term

d : \Pi_{(x : A)} \Pi_{(y : C(x))} \Sigma_{(p : x_0 = x)}~\mathsf{trans}(p, r) = y

then the map x \mapsto \pi_1(d(x)): C(x) \to (x_0 = x) is an equivalence for each x : A.

We can use the encode-decode method to show that the type family C : \mathbb{S}^1\to{} U described by \mathbb{Z} and the successor map is fiberwise equivalent to the family of paths to the base point. So we have to find a term of type

\Pi_{(x : S^1)}\Pi_{(y : C(x))}\Sigma_{(p : x_0 = x)}~\mathsf{trans}(p, r) = y.

By the inductive principle of the circle, it suffices to find terms

T : \Pi_{(n : \mathbb{Z})}\Sigma_{(p : x_0 = x)}~\mathsf{trans}(p, r) = n
q : \mathsf{trans}(\mathsf{loop}, T) = T.

We define T(n) := (\mathsf{loop}^n, ! : \mathsf{succ}^n(0) = n). Then note that

\mathsf{trans}(\mathsf{loop}, T)(n) = \mathsf{trans}(\mathsf{loop}, T(n + 1)).

To show that it is equal to T(n), we only need to show that their first components are equal, because \mathbb{Z} is a set. And it is easy to verify that \mathsf{trans}(\mathsf{loop}, \mathsf{loop}^{n+1}) = \mathsf{loop}^{n+1} \cdot \mathsf{loop}^{-1} = \mathsf{loop}^n.

The encode-decode method, which we have illustrated in the case of the circle, is THE MOST IMPORTANT WAY of finding a new description of the path space of a type. But it is not the only way. In the following, we will illustrate another method of identifying the path space of the 2-sphere.

The type theoretical n-spheres can be introduced as higher inductive types, just as the circle. The idea behind the definition of the (n+1)-sphere is that it has one base point, and then we attach an (n+1)-dimensional disk to it by gluing its boundary to the point. Recall that the boundary of the (n+1)-dimensional disk is the n-sphere, and we can imagine the (n+1)-dimensional disk to be an n-sphere together with a point and one path from this point to each of the points of on the boundary. This process describes a pushout diagram 1 \leftarrow S^n \rightarrow D^{n+1}. Since D^{n+1} is contractible, we might as well replace it by a point, but then we must take the homotopy pushout. However, in type theory everything is up to homotopy, so this is a completely innocent operation. A pushout of the span 1 \leftarrow{} X \rightarrow{} 1 has a special name: the suspension of X. Thus, we have just described the (n+1)-sphere as the suspension of the n-sphere. In type theory, we do this as follows:

\mathsf{N}   : S^{n+1}
\mathsf{S}   : S^{n+1}
\mathsf{eqt} : S^n \to (N =_{S^{n+1}} S).

Just as the circle, the (n+1)-sphere is given an inductive principle. Let P \twoheadrightarrow{} S^2 be a family of types over S^2. To construct a section of P, we must find

x_{\mathsf{N}} : P (\mathsf{N})
x_{\mathsf{S}} : P (\mathsf{S})
p   : \Pi_{(t : S^1)}~\mathsf{trans}(\mathsf{eqt}(t), x_{\mathsf{N}}) =_{P(\mathsf{S})} x_{\mathsf{S}}.

Our goal is now to study the path fibration \mathsf{N} : 1 \twoheadrightarrow{} S^2 of the 2-sphere. In particular, we want to give a new, independent description of this fibration. However, for that to be possible we need to know how to define new fibrations over S^2. In other words, we need to know how to map from S^2 into the universe of all types. A map from S^2 into U is the same thing as a section of the trivial fibration S^2 \times{} U \twoheadrightarrow{}S^2. Hence, by the inductive principle, a map into the universe consists of

A : U
B : U
e : S^1\to{} (A =_U B).

Thus, with the univalence axiom, we can construct a type family over S^2 by defining

A : U
B : U
e : S^1 \to{} (A \simeq{} B)

Thus, we describe a fibration by describing its descent data, and of course these two descriptions are itself equivalent (the descent property).

Recall that the path fibration (based at \mathsf{N}) of S^2 is the initial fibration P with a point x : P(\mathsf{N}). By the descent property, it follows that the path fibration is the initial quadruple of the form (A, B, e, a), consisting of A, B and e as above, and a in A. (Of course, there is a theorem behind this, that these two notions of initiality agree.) We can simplify this even further.

Recall that a map from S^1 to a type X is the same thing as a section of the trivial fibration S^1 \times{} X \twoheadrightarrow{} S^1. So we may use the inductive principle of S^1 to eliminate out of S^1. To describe a map from S^1 into X we need

x : X
l : x =_X x

And the type of such pairs (x, l) is of course canonically equivalent to the type of maps S^1 \to{} X. So we see that a type family over S^2 is equivalently described by four pieces of data:

A : U
B : U
e : A \simeq{} B
h : e =_{(A \simeq{} B)} e.

The latter type is itself equivalent to the type e \sim{} e of homotopies from e to itself. Furthermore, since (A =_U B) \to{} (A \simeq{} B) is an equivalence, the type of pairs (B, e) as above is equivalent to the total space of paths in U starting at A, which is contractible. Its center of contraction is the pair (A, id). Our final equivalent description of a type family over S^2 is therefore to provide:

A : U
h : id \sim{} id.

Moreover, the path fibration is the initial type family with a point above \mathsf{N}. It is therefore given as a higher inductive type \Omega S^2 with

r : \Omega S^2
h : \Pi_{(x : \Omega S^2)}~ x =_{\Omega S^2} x.

In a similar way, one can show that \Omega S^1 is the initial space with a point and an automorphism (i.e. an equivalence to itself), which is therefore an equivalent description of \mathbb{Z}.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s