Homotopy Type Theory
James construction


The James construction JAJ A on a pointed type AA. Is the higher inductive type given by


We have an equivalence of types JAΩΣAJA \simeq \Omega \Sigma A if AA is 0-connected.

We can see that JAJ A is simply the free monoid on AA. 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 nA) n:(J_n A)_{n: \mathbb{N}} together with maps (i n:J nAJ n+1A) n:(i_n : J_n A \to J_{n+1} A)_{n:\mathbb{N}} such that the type J AJ_\infty A defined as the sequential colimit of (J nA) n:(J_n A)_{n:\mathbb{N}} is equivalent to JAJ A.

This is useful as we can study the lower homotopy groups of ΩΣX\Omega \Sigma X by studying the lower homotopy groups of the sequential colimit. Which is what allows Brunerie to show π 4(S 3)=/n\pi_4(S^3) = \mathbb{Z} / n \mathbb{Z}.


category: homotopy theory