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^{n}), π_{3}(S^{2}), and π_{4}(S^{3}); 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 (π_{4}(S^{3})) 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 π_{1}(S^{1}) is Z and that π_{k}(S^{1}) is trivial otherwise (by Mike Shulman), and a proof that π_{k}(S^{n}) 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
^{0}is the booleans, so these calculations follow from Hedberg’s theorem, which entails that the booleans are a set.

- In the second row, S
^{1}is the circle. Our calculation of this row consists of showing that the loop space of the circle (Ω(S^{1})) is Z: Applying truncation to both sides shows that π_{1}(S^{1}) 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^{1}) 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^{n}) diagonal) state that π_{k}(S^{n}) 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^{1}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, Ω^{n}(A), by induction on n. Then, we define the n-sphere to be a higher inductive type with one point and one element of Ω^{n}. 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^{n}, but the level of iteration of the path type depends on n, and when n is a variable, Ω^{n}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^{n}) (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 π_{1}and then uses the Freudenthal suspension theorem (see below) to induct up. - For a long time after the first proof of π
_{1}(S^{1}) 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 π_{2}(S^{2}) (by Guillaume Brunerie), which goes by way of proving that the total space of the Hopf fibration (as constructed by Peter Lumsdaine) is S^{3}. This gives π_{2}(S^{2}), and also implies that π_{k}(S^{2}) = π_{k}(S^{3}), for k>=3. Because we have now calculated π_{3}(S^{3}) (see below), this gives π_{3}(S^{2}) = Z. Because we have now calculated most of π_{4}(S^{3}) (see below; the “most of” disclaimer is why these squares are shaded white in the table), this gives most of π_{4}(S^{2}). The grey shading on the remainder of the S^{2}/S^{3}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 π_{2}(S^{2}), 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^{1}. This proof bypasses showing that the total space of the Hopf fibration is S^{3}, 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^{2}, but we eventually developed an encode-decode proof (also by Dan Licata) for the suspension definition. - Next, we have the π
_{n}(S^{n}) = Z diagonal. The proof is by induction on n, using π_{1}(S^{1}) in the base case, and proving that π_{n}(S^{n}) = π_{n+1}(S^{n+1}) 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 π_{2}(S^{2}). 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^{n}), for π_{n}(S^{n}), and for π_{n+1}(S^{n}) (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^{n}) with the homotopy-theoretic notion of connectedness of maps and spaces. Indeed, the tower of results going from π_{2}(S^{2}) to π_{n}(S^{n}) to Freudenthal really illustrates the promise of the interaction between homotopy theory and type theory: we started with a more homotopy-theoretic proof of π_{2}(S^{2}), which led to a more type-theoretic proof of π_{2}(S^{2}) (using the encode-decode method), which led to a more type-theoretic proof of π_{n}(S^{n}), 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^{n}) = Z_{2}diagonal, we have a proof (by Guillaume Brunerie) that there exists a k such that π_{4}(S^{3}) = 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^{n}) = 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 π
_{1}(S^{1}), 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:

- Many of these results are written up in an informal style in the forthcoming book
*Homotopy Type Theory: Univalent Foundations of Mathematics* - 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

- Some individual results/tools have been written up:
- For π
_{1}(S^{1}), see these blog posts, and this paper. - Covering spaces
- Higher inductive types
- How to fake higher inductive types in current proof assistants
- Truncations

- For π
- 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).

Great work! I’m interested in getting involved. Is there a list of low-hanging fruit somewhere?

In case of coqiphiles, I’d heard there was a difficulty about saying “Delta Set” in coq… I haven’t resolved that particular question as such, but maybe reduced some of the opacity, in the sense that coq can produce some Type, dependent on a natural number k, that obviously ought to be the k-skeleton of a Delta set; on the other hand, discerning *what* that thing actually asks for is, to say the least, daunting, but not quite totally incomprehensible.

here is the gist of it. Enjoy!

oh, on the plus side, it’s clear that the first part of a DeltaSkeleton (S k) is its underlying (DeltaSkeleton k); so, not a total loss.

Hi! I had a very brief look at your code. What you are doing seems to be (at least) very similar to an approach that a couple of people try, or have tried. It is normal to think that this should definitely work and it’s just a matter of actually doing it, but I am not sure about that anymore. It is very hard to describe what goes wrong and/or I do not understand the problem. It seems that, in order to define certain functions, one already needs to know that these (or other) functions behave “functorially” on lower levels. That is something one can show easily, but by doing so, one introduces nontrivial paths and the horror with coherences begins – even if everything is “obviously well-founded” (recall that the whole idea here is to use the directedness of the Delta_i category for avoiding coherence problems!).

I am not convinced that this approach cannot be completed, but neither am I convinced that it can. If it does not work, it would be really valuable to understand what the underlying reason is. Together with Nuo Li and Paolo Capriotti, I also have a git repository about this stuff (we use Agda), but it’s a total mess (I’ll post a link if we ever make progress and clean it up).

Here is maybe one positive thing I can say: Instead of your type chooseType for (n C k), try using strictly monotonous functions between finite ordered sets. Your composition of binominal coefficients then becomes literal composition of functions. E.g. to get a sub-skeleton, you just need to compose with the function that tells you which k of the skeleton’s n points/vertices you want to keep. At least, this works quite neatly for us.

I was avoiding function types because, even for functions between finite decidable-equality sets, deriving anything like decidable equality of functions is difficult — I suppose this means coq could be told to agree two implementations of a function were different if they had provably-different complexity… and in the end I had to toss in decidable equality as an axiom anyways!

I think I just want to emphasize that the things supposed equal in the last recursion — the thing that looks like functoriality where I give up and throw in “admit” — isn’t functoriality for an

assumedDelta set, but for thederiveddelta-set of n-filled l-simplices, which is why I have some hope that it could actually be finished, if one could replace the “assert” interaction with an explicit term…In the process I’ve come to a better appreciation of the dependences actually involved, which suggests that the notion itself is of limited computational use: in a general delta set, an explicit term for an n-cell will involve explicit terms for k-cells in lower degree before you can even name the type of the last filling, and each of those (n C k) k-cells needs to describe its type, each of which … maybe we are saved by not needing quite all that dependency in practical cases. On the other hand, Delta Sets are built on hyper-cubic diagrams, which have permutahedra describing all the equalities involved; but for surprisingly many things, associahedra can do instead of permutahedra, while having rather fewer vertices — I can’t be sure of the cells altogether yet — and so one should look for the diagrams that are to associahedra as cubes are to permutahedra, and then we’ll really be getting somewhere.

Yes, the fact that one needs functoriality only for an actually *constructed* Delta set is what also gives me some hope here. It will certainly not be easy though: for example, your “Axiom listsubsetsubseteq” will probably cause problems as it postulates an inhabitant of a type that is in general not propositional. I would be very surprised if it was enough to ensure that there is this categorical structure; what we probably need is an omega-categorical structure. That’s what I meant by “horror with coherences”. My hope would be that we can get these coherences automatically, if we prove “listsubsetsubseteq” in a “good” way – but I don’t know. Reading what you described in the end, I guess you also have something like this in mind.

About the other thing, I think it is possible to use functions between finite sets and assume functional extensionality for those. If everything works in the end, one can encode these functions such that no assumption is needed anymore. Fair enough, one can also use such an encoding right from the beginning. I just wanted to do it first in a setting with less obfuscation. “Complexity” is a meta-theoretic concept, we can’t talk about that internally.

Regarding the open problem of constructing the senior Hopf fibration in homotopy type theory, have we proven that the 3-sphere is a h-space? Or is it not yet computed that the self-join of the 3-sphere is the 7-sphere?

Since the n-sphere is n-fold self-join of the 0-sphere, the latter question boils down to an associator equivalence for joins of three things, and an ordinary induction argument. It shouldn’t be more difficult than the coequalizer flattening lemma, if it isn’t written already.

Mike has some way of talking about localizations as inductive constructions, so another interesting question is writing the proof that invert-prime-2-spheres are H-spaces. One of my own games recently has been to write the definition of An-structure on a space (because it can be stated in terms of pullback squares and perhaps equivalences), but in the connection with An-*forms* there are anticipated troubles.

No, we haven’t proved that the 3-sphere is an h-space and it’s indeed the only thing missing to construct the senior Hopf fibration.

As Jesse said, once you have associativity of the join it’s easy to prove that S^3 * S^3 = S^7. Note, though, that associativity of the join is (currently) much more difficult to formalize than the flattening lemma. We have at least two different formalized proofs of the flattening lemma but none of associativity of the join (but we’re working on it!).

much more difficult, eh? That’s irksome… OK, let me see where my intuition went funny…

Oh, one needs to build two 2-homotopies (or two coherent cubical diagrams) and then argue that they’re the same, so a 3-homotopy between them, then repeat the argument backwards, and then… no wonder, and I beg your pardon. On The Other Hand, both 2-homotopies can be made (trivial) instances of flattening (for pushouts rather than coequalizers, so someone quicker than I am should finish the presentation of pushouts and the pushout flattening lemma), which ought to save something, but maybe you already have…

I’m not sure what you’re talking about, I’m only talking about proving (A * B) * C = A * (B * C) and I don’t see how you can use the flattening lemma for that (you do need the flattening lemma for pushouts in the construction of the Hopf fibration, but at a different place)

Intuitively it’s very easy, you just have to define the two maps back and forth and prove that they are inverse to each other by induction.

The problem is that currently we don’t know how to implement (in an existing proof assistant) definitional computation rules for path constructors of higher inductive types and some related beta-like reductions (like ap (fun x => x) p = p). Actually, we don’t even know whether it’s consistent to have them definitionally instead of propositionally.

One consequence is that you often have to do the reductions by hand which can be quite tedious (it’s the case for the flattening lemma), but sometimes it’s even worse because you also have to prove coherence conditions between those “reduction rules” and that’s really heavy and not pretty.

Our current model construction for HITs does seem to produce “definitional” computation rules, of a sort, for path constructors. The twist is that they’re definitional with respect to a notion of “dependent path” and “ap” that are only propositionally the same as those we usually define using transport and path induction.

I was refering to what happens on paper when unwrapping the definitions of (A * B) * C and A * (B * C); the projection map (A * B ) C -> A * B wants to be realized as the map of pushouts from the pushout of A B C -> A C and A B C -> B C; that it really is just the projection is, I’m sure, a triviality… but the shape of either map (A * B ) * C -> A * (B * C) will involve 3-homotopies and the section/retraction at either end will probably need a 4-homotopy from something to zero. These are, I’m sure, the coherences you mention. I’m just trying to keep track of the dimensions of things, because things only seem to get worse above dimension 2.

The equivalences is even more intuitively obvious if we say/argue that (A * B ) * C and A * ( B * C ) are both the initial thing X under A, B, and C such that the three coordinates A B C -> ? -> X. coherently agree, but I don’t know if that saves any scripting. This makes me wonder if one could/should tacticalize initiality arguments of exactly this sort…