Contents

# Contents

## Idea

The James construction type is an axiomatization of the James construction in the context of homotopy type theory.

## Definition

As a higher inductive type, the James construction type $J A$ of a pointed type $(A, a)$ is given by the following constructors

• $\epsilon_{J A} : J A$
• $\alpha_{J A} : A \to J A \to J A$
• $\delta_{J A} : \prod_{x : J A} x = \alpha_{J A}(a)(x)$

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

## Properties

There is an equivalence of types $J A \simeq \Omega \Sigma A$ if $A$ is 0-connected.

## References

Created on June 7, 2022 at 21:38:02. See the history of this page for a list of all contributions to it.