Egbert Rijke: The loop space of the 2-sphere

Egbert Rijke
Carnegie Mellon University 

Abstract: Homotopy Type Theory comes with new tools to do some fun homotopy theory with. First, the univalence axiom makes it easy to find classifying spaces, and higher inductive types allow us to define new spaces by specifying points and paths in the same way that algebras may be defined by generators and relations. The spheres can be described this way: The (n+1)-sphere has a north and a south pole, and an equator which adds a path from north to south for every x in the n-sphere. Although the computation of the homotopy groups of spheres in HoTT seems to be just as complicated as in the the classical theory, we can compute the actual loop spaces of the the spheres using higher inductive types. For instance, the description of the loop space of the 2-sphere as HIT is: the initial pointed space with a homotopy id ~ id.