Homotopy Type Theory
James construction (Rev #8)


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

  • ϵ JA:JA\epsilon_{JA} : JA
  • α JA:AJAJA\alpha_{JA} : A \to JA \to JA
  • δ JA: x:JAx=α A(* A,x)\delta_{JA} : \prod_{x : JA} x = \alpha_A (*_A, x)


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

We can see that JAJA 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 JAJA.

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

Revision on September 4, 2018 at 09:38:31 by Ali Caglayan. See the history of this page for a list of all contributions to it.