A little while ago, we gave an overview of the kinds of results in homotopy theory that we might try to prove in homotopy type theory (such as calculating homotopy groups of spheres), and the basic tools used in our synthetic approach to the subject (such as univalence and higher inductive types).   The big open questions are: How much homotopy theory can one do in this synthetic style? And, how hard is it to work in this style, and to give computer-checked proofs of these results?

Thus far, our results have been quite encouraging on both of these fronts: We’ve done a significant swath of basic homotopy theory synthetically, including calculations of  π_n(Sⁿ),  π₃(S²),  and π₄(S³); proofs of the Freudenthal suspension theorem, the Blakers-Massey theorem, and van Kampen’s theorem; a construction of Eilenberg-Mac Lane spaces; and a development of the theory of covering spaces.  We’ve given computer-checked proofs for almost all of these results, and the process has been quite pleasant and fun.  Lengthwise, the computer-checked proofs are comparable with, and in some cases shorter than, the same proof written out in a traditional style.    Moreover, the proofs have involved a blend of classical homotopy theoretic ideas and type theoretic ideas.  While most of what we have done is to give new proofs of existing results, these techniques have started to lead to new results, such as a proof of the Blakers-Massey theorem in general ∞-topoi (which we gave by translating the type-theoretic proof).  Additionally, we have one example (π₄(S³)) illustrating the promise of the constructive aspects of homotopy type theory.  Finally, these proofs have furthered our understanding of the computational aspects of homotopy type theory, particularly about computing with higher identity types.

This post will describe the results that we’ve gotten so far—particularly this spring, during the special year at IAS.  This was a big collaborative effort: many people contributed to it, by being the principal author of a proof or formalization, by suggesting problems to work on, by giving feedback on results, or by contributing to discussions and seminars. When the spring IAS term started on January 14th, we had a proof that π₁(S¹) is Z and that π_k(S¹) is trivial otherwise (by Mike Shulman), and a proof that π_k(Sⁿ) is trivial for k<n (by Guillaume Brunerie).  Here’s what that looks like in the chart of homotopy groups of spheres:

And, here’s what we had proved about homotopy groups of spheres by the end of the term (we’ll explain the grey/white highlights below):

Let’s go through the theorems that fill in this table:

• In the first row, S⁰ is the booleans, so these calculations follow from Hedberg’s theorem, which entails that the booleans are a set.
  
• In the second row, S¹ is the circle.  Our calculation of this row consists of showing that the  loop space of the circle (Ω(S¹)) is Z: Applying truncation to both sides shows that  π₁(S¹) is Z.  Moreover, because the higher homotopy groups of a type are constructed from the loop space of that type, we get that that the higher homotopy groups of the circle are the same as the higher homotopy groups of Z, and therefore trivial, again because Z is a set.
  We have a few different proofs that Ω(S¹) is Z.  The first (by Mike Shulman), follows a standard homotopy-theoretic argument, showing that the total space of the universal cover of the circle is contractible.  Another (by Guillaume Brunerie) shortens the original proof significantly, by factoring some of the reasoning out into a flattening lemma about total spaces of fibrations defined by recursion on higher inductives.  Another proof (by Dan Licata) avoids calculating the total space of the cover, instead relying on calculations using the definition of the cover by circle recursion.  The template introduced in this proof is now known as the encode-decode method.
• The all-0 diagonals (the colored diagonals below the π_n(Sⁿ) diagonal) state that π_k(Sⁿ) is trivial for k<n.  We have a few different proofs of this now.  In fact, we have two definitions of the n-sphere (which should coincide, but we haven’t proved this yet). The first is by induction on n: S¹ is the circle, and the (n+1)-sphere is the suspension of the n-sphere.  The second uses a fancy form of higher inductive types: First, we define the n-fold iterated loop space of a type, Ωⁿ(A), by induction on n. Then, we define the n-sphere to be a higher inductive type with one point and one element of Ωⁿ.  The circle is generated by a point and a single 1-dimensional loop; the 2-sphere by a single point and a single 2-dimensional loop, and so on.  This form of higher-inductive type is a bit unusual (and has not been formally studied): for each instantiation of n, the n-loop constructor is an element of a path type of Sⁿ, but the level of iteration of the path type depends on n, and when n is a variable, Ωⁿ is not syntactically a path type.  However, the fact that the homotopy groups have come out right so far provides some indication that this is a sensible notion.
  The first proof of π_k<n(Sⁿ) (by Guillaume Brunerie), for the suspension definition of the spheres, uses a connectedness argument.  The second (by Dan Licata), for the iterated-loop-space definition, uses the encode-decode method.  A third (by Dan Licata) uses a connectedness argument for π₁ and then uses the Freudenthal suspension theorem (see below) to induct up.
• For a long time after the first proof of π₁(S¹) in spring 2011, we were stuck on calculating any non-trivial higher homotopy groups.  The thing that really broke the dam open on these was a proof of π₂(S²) (by Guillaume Brunerie), which goes by way of proving that the total space of the Hopf fibration (as constructed by Peter Lumsdaine) is S³.  This gives π₂(S²), and also implies that π_k(S²) = π_k(S³), for k>=3. Because we have now calculated π₃(S³) (see below), this gives π₃(S²) = Z.  Because we have now calculated most of  π₄(S³) (see below; the “most of” disclaimer is why these squares are shaded white in the table), this gives most of π₄(S²).  The grey shading on the remainder of the S²/S³ rows indicates that while we have not calculated any of these groups, we know that the two rows are equal.
  The calculation of the total space of the Hopf fibration has proved difficult to formalize, because a key lemma requires some significant path algebra.  However, only a couple of days after the first proof of π₂(S²), we had a computer-checked one (by Dan Licata), using the encode-decode method, with the Hopf fibration playing the same role that the universal cover plays for S¹.  This proof bypasses showing that the total space of the Hopf fibration is S³, so it doesn’t give all the nice corollaries mentioned above.  But it also illustrates that type theory can lead to shorter and more “beta-reduced” proofs of these theorems.  This proof was for the iterated-loop-space definition of S², but we eventually developed an encode-decode proof (also by Dan Licata) for the suspension definition.
• Next, we have the π_n(Sⁿ) = Z diagonal.  The proof is by induction on n, using π₁(S¹) in the base case, and proving that π_n(Sⁿ) = π_n+1(Sⁿ⁺¹) in the inductive step. We have a couple of proofs of this.  The first (by Dan Licata and Guillaume Brunerie) is a generalization of the encode-decode proof of π₂(S²).  It took about two weeks to develop and formalize the proof, much of which is a library exploring the type theory of iterated loop spaces.  The second proof, for the suspension definition of the spheres, uses the Freudenthal suspension theorem.
  
• The Freudenthal suspension theorem gives the connectedness of the path constructor for suspensions.  It implies that all entries in the colored diagonals in the above chart are the same.   Therefore, it suffices to compute one entry in each diagonal.  We have done this for π_k<n(Sⁿ), for π_n(Sⁿ), and for π_n+1(Sⁿ) (shaded white).  The remaining diagonals are shaded grey because we have proved that all entries are the same, but we haven’t calculated any individual entry.
  The proof of the Freudenthal suspension theorem (by Peter Lumsdaine; formalized by Dan Licata) is an interesting combination of the encode-decode method used in π_n(Sⁿ) with the homotopy-theoretic notion of connectedness of maps and spaces.  Indeed, the tower of results going from π₂(S²) to π_n(Sⁿ) to Freudenthal really illustrates the promise of the interaction between homotopy theory and type theory: we started with a more homotopy-theoretic proof of π₂(S²), which led to a more type-theoretic proof of π₂(S²) (using the encode-decode method), which led to a more type-theoretic proof of π_n(Sⁿ), which led to a proof of the Freudenthal suspension theorem that combines these type-theoretic aspects with some additional homotopy-theoretic ideas about connectedness.    
• In the π_n+1(Sⁿ) = Z₂ diagonal, we have a proof (by Guillaume Brunerie) that there exists a k such that π₄(S³) = Z_k, using the James construction.  This diagonal is shaded white because this isn’t quite the classical result: we should also check that k is 2.  However, this proof illustrates the promise of a computational interpretation of homotopy type theory: the proof is constructive, so to check that k is indeed 2, all we would need to do is run the program!

In addition to homotopy groups of spheres, we have proved the following theorems:

• The Freudenthal suspension theorem gives information about spaces other than spheres.  For example, we have a construction (by Dan Licata) of Eilenberg-Mac Lane spaces K(G,n), which are a basic building block that can be used to construct spaces up to homotopy equivalence.  For an abelian group G, K(G,n) is a space whose nth homotopy group is G, and whose other homotopy groups are trivial; for example, K(Z,n) is equivalent to the n-truncation of the n-sphere. We first construct K(G,1), and then construct K(G,n) by suspending K(G,1) and truncating.  The proof that it has the right homotopy groups uses the Freudenthal suspension theorem, generalizing the proof from Freudenthal that π_n(Sⁿ) = Z.
• The Freudenthal suspension theorem gives the connectivity of the path constructor of a suspension.  A generalization of suspensions is the notion of a pushout, and the generalization of Freudenthal to pushouts is the Blakers-Massey theorem.   We have a proof of Blakers-Massey (by Peter Lumsdaine, Eric Finster, and Dan Licata; formalized by Favonia).  We have also translated this proof to the language of  ∞-topoi, which proves the result in a more general setting than was previously known.  
• van Kampen’s theorem characterizes the fundamental group of a pushout.  We have a proof (by Mike Shulman; formalized by Favonia) using the encode-decode method.  
• To calculate π₁(S¹), we used the universal cover of the circle.  This is an instance of a  general notion of covering spaces, and the fact that covering spaces of a space correspond to actions by its fundamental group.  Favonia formulated and formalized the theory of covering spaces.

You can find out more about these results in the following places:

1. Many of these results are written up in an informal style in the forthcoming book  Homotopy Type Theory: Univalent Foundations of Mathematics
2. There are many videos of talks on these results:
   • A good place to start is this end-of-the-term lecture summarizing the results.
   • A Computer-Checked Proof that pi_1(S^1) is Z
   • The Hopf Fibration via Higher Inductive Types
   • pi_2(S^2) in HoTT
   • The James Construction and pi_4(S^3)
   • Eilenberg-Mac Lane Spaces in HoTT
   • Cohomology in Homotopy Type Theory
   • Formal Abstract Homotopy Theory
   • Toward Higher Inductive Types
   • Semantics of Higher Inductive Types
3. Some individual results/tools have been written up:
   • For π₁(S¹), see these blog posts, and this paper.
   • Covering spaces
   • Higher inductive types
   • How to fake higher inductive types in current proof assistants
   • Truncations
4. All of the computer-checked proofs are available online; see here and here and here.  This wiki page has pointers to specific results.

Finally, there is a lot of low-hanging fruit left to pick!  If you are interested in getting involved, leave a comment, or send an email to someone mentioned above (or to the HomotopyTypeTheory google group).