The James construction and $\pi_4(\mathbb{S}^3)$ in homotopy type theory

TL;DR

This paper formalizes the James construction within homotopy type theory using Agda and employs it to constructively prove that the fourth homotopy group of the 3-sphere is cyclic of some order, without explicitly computing that order.

Contribution

It provides the first formalization of the James construction in homotopy type theory and demonstrates its application in a constructive proof of a key homotopy group property.

Findings

Formalization of James construction in Agda

Constructive proof that π₄(S³) ≅ Z/nZ

Techniques for formalizing homotopy-theoretic concepts

Abstract

In the first part of this paper we present a formalization in Agda of the James construction in homotopy type theory. We include several fragments of code to show what the Agda code looks like, and we explain several techniques that we used in the formalization. In the second part, we use the James construction to give a constructive proof that $\pi_4(\mathbb{S}^3)$ is of the form $\mathbb{Z}/n\mathbb{Z}$ (but we do not compute the $n$ here).