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.
Homotopy Type Theory 
Nice proof! I like how the induction step of
boils down to a sequence of structural interactions between loop spaces and truncations (plus the Freudenthal-like main lemma via encode-decode).
A few comments regarding your loop space library:
* The result about higher loops in types is precisely the local-global looping principle (Lemma 4.2) from the universe truncation level article by Nicolai Kraus and myself (Lemma 1 in our old blog post). There is a subtle issue regarding its implementation in Agda, which you conveniently avoid by assuming Type-in-Type: you can’t really write the equality
((a : A) -> Loop n A a) = (Loop (S n) Type A)because the right side lives in a universe one level higher than the left one, and Agda doesn’t have cumulative universes.* For our article, we developed a small library for pointed types and loop spaces, which seems to overlap with yours quite a bit. We tried to keep things modular, working with pointed equivalences where possible, and even introducing connectives
and 
on pointed types. For example, the characterization of higher loops in Pi-types as Pi-types of higher loops is essentially just one-liners, avoiding extensive calculations like here.
It would be interesting to compare the two approaches and merge the respective results. But I am pretty sure your 1500 lines of code can be reduced to well below 600!