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 can be described either as the set of unit vectors of , or equivalently as the suspension of . Likewise, can be described as the suspension of . 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 of free loops in . The loop space of the sphere turns out to be the (homotopy) initial triple consisting of a space with a base point 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 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

.

It turns out that paths have many things in common with equality. For instance, the path fibration is the homotopy initial reflexive fibration (i.e. with a map 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 says that to find a section of a fibration

, we must find a point above the base point, and show that the other endpoint of the lift at of matches with . In type theory, we say this as follows:

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 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 by specifying

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 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 with is equivalent to paths to , it suffices to show that the total space of is contractible, with center of contraction . To show that the total space of is contractible, we have to find a term of type

.

The type of identifications is equivalent to the type . Thus, we have the following theorem.

**Theorem (encode-decode method).**

Let be a type with a base point . Let be a type family over with . If we have a term

then the map is an equivalence for each .

We can use the encode-decode method to show that the type family described by 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

.

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

.

We define . Then note that

.

To show that it is equal to , we only need to show that their first components are equal, because is a set. And it is easy to verify that .

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 . Since 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 has a special name: the suspension of . Thus, we have just described the (n+1)-sphere as the suspension of the n-sphere. In type theory, we do this as follows:

.

Just as the circle, the (n+1)-sphere is given an inductive principle. Let be a family of types over . To construct a section of , we must find

.

Our goal is now to study the path fibration 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 . In other words, we need to know how to map from into the universe of all types. A map from into is the same thing as a section of the trivial fibration . Hence, by the inductive principle, a map into the universe consists of

.

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

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 ) of is the initial fibration with a point . By the descent property, it follows that the path fibration is the initial quadruple of the form , consisting of , and as above, and in . (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 to a type is the same thing as a section of the trivial fibration . So we may use the inductive principle of to eliminate out of . To describe a map from into we need

And the type of such pairs is of course canonically equivalent to the type of maps . So we see that a type family over is equivalently described by four pieces of data:

.

The latter type is itself equivalent to the type of homotopies from to itself. Furthermore, since is an equivalence, the type of pairs as above is equivalent to the total space of paths in starting at , which is contractible. Its center of contraction is the pair . Our final equivalent description of a type family over is therefore to provide:

.

Moreover, the path fibration is the initial type family with a point above . It is therefore given as a higher inductive type with

.

In a similar way, one can show that is the initial space with a point and an automorphism (i.e. an equivalence to itself), which is therefore an equivalent description of .