## Definition ## The James construction $JA$ on a pointed type $A$. Is the higher inductive type given by * $\epsilon_A : JA$ * $\alpha_A : A \to JA \to JA$ * $\delta_J : \prod_{x : JA} \to x = \alpha_A (*_A, x)$ ## Properties ## We have an equivalence of types $JA \simeq \Omega \Sigma A$ We can see that $JA$ is simply the free monoid on $A$. The higher inductive type is recursive which can make it difficult to study. This however can be remedied by defining a sequence of types $(J_n A)_{n: \mathbb{N}}$ together with maps $(i_n : J_n A \to J_{n+1} A)_{n:\mathbb{N}}$ such that the type $J_\infty A$ defined as the sequential colimit of $(J_n A)_{n:\mathbb{N}}$ is equivalent to $JA$. This is useful as we can study the lower homotopy groups of $\Omega \Sigma X$ by studying the lower homotopy groups of the sequential colimit. Which is what allows Brunerie to show $\pi_4(S^3) = \mathbb{Z} / n \mathbb{Z}$. ## References ## * [The James construction and $\pi_4(S^3)$ in homotopy type theory](https://arxiv.org/abs/1710.10307) * [On the homotopy groups of spheres in homotopy type theory](https://arxiv.org/abs/1606.05916)