Homotopy Type Theory
James construction (changes)

Showing changes from revision #8 to #9: Added | Removed | Changed


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

  • ϵ JAJA: JA JA \epsilon_{JA} \epsilon_{J A} : JA J A
  • α JAJA:A JA JA JA JA \alpha_{JA} \alpha_{J A} : A \to JA J A \to JA J A
  • δ JAJA: x: JA JAx=α A(* A,x) \delta_{JA} \delta_{J A} : \prod_{x : JA} J A} 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 JA JA JA J 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 JA JA JA J 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

Last revised on September 4, 2018 at 12:59:39. See the history of this page for a list of all contributions to it.