Homotopy Type Theory James construction > history (Rev #5)

Definition

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

  • ϵ A:JA\epsilon_A : JA
  • α A:AJAJA\alpha_A : A \to JA \to JA
  • δ J: x:JAx=α A(* A,x)\delta_J : \prod_{x : JA} x = \alpha_A (*_A, x)

Properties

We have an equivalence of types JAΩΣAJA \simeq \Omega \Sigma A

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}.

References

category: homotopy theory

Revision on August 27, 2018 at 11:59:59 by Anonymous?. See the history of this page for a list of all contributions to it.