natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
The James construction type is an axiomatization of the James construction in the context of homotopy type theory.
As a higher inductive type, the James construction type $J A$ of a pointed type $(A, a)$ is given by the following constructors
In Coq pseudocode this becomes
Inductive JamesConstruction (A : PointedType) : Type
| epsilon : JamesConstruction A
| alpha : A -> JamesConstruction A -> JamesConstruction A
| delta : forall (x : JamesConstruction A) x = alpha point x
We can see that $J A$ 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 $J A$.
There is an equivalence of types $J A \simeq \Omega \Sigma A$ if $A$ is 0-connected.
Guillaume Brunerie, On the homotopy groups of spheres in homotopy type theory (arxiv:1606.05916)
Peter LeFanu Lumsdaine, Mike Shulman, Semantics of higher inductive types (arXiv:1705.07088)
Guillaume Brunerie, The James construction and $\pi_4(S^3)$ in homotopy type theory (arXiv:1710.10307)
Created on June 7, 2022 at 21:38:02. See the history of this page for a list of all contributions to it.