I’m giving a talk this week at CPP. While I’m going to talk more broadly about applications of higher inductive types, for the proceedings, Guillaume Brunerie and I put together an “informalization” of πn(Sn), which you can find here.
This is a different proof of πn(Sn) than the one in the HoTT book—this is the first proof we did, which led Peter Lumsdaine to prove the Freudenthal suspension theorem, which is used in the proof in the book. This proof is interesting for several reasons:
- Calculating πn(Sn) is a fairly easy theorem in algebraic topology (e.g. it would be covered in a first- or second-year graduate algebraic topology course), but it is more complex than many of the results that had previously been proved in homotopy type theory. For example, it was one of the first results about an infinite family of spaces, of variable dimension, to be proved in homotopy type theory.
- When doing homotopy theory in a constructive/synthetic style in homotopy type theory, there is always the possibility that classical results will not be provable—the logical axioms for spaces might not be strong enough to prove certain classical theorems about them. Our proof shows that the characterization of πn(Sn) does follow from a higher-inductive description of the spheres, in the presence of univalence, which provides evidence for the usefulness of these definitions and methods.
- This is one of the first examples of computation with arbitrary-dimensional structures that has been considered in homotopy type theory. It would be a good example for the recent work on a constructive model in cubical sets by Coquand, Bezem, and Huber.
- The proof is not a transcription of a textbook homotopy theoretic proof, but mixes classical ideas with type-theoretic ones. The type-theoretic techniques used here have been applied in other proofs.
- We give a direct higher-inductive definition of the n-dimensional sphere Sn as the free type with a base pointbase and a loop in Ωn Sn). This definition does not fall into the collection of higher inductive types that has been formally justified by a semantics, because it involves a path constructor at a variable level. However, our result shows that it is a useful characterization of the spheres to work with, and it has prompted some work on generalizing schemas for higher inductive types to account for these sorts of definitions.
The Agda version is available on GitHub (tag pinsn-cpp-paper). The proof includes a library of lemmas about iterated loop spaces that is independent of the particular application to n-dimensional spheres.