James construction type
Quentin
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 of a pointed type is given by the following constructors
In Rocq pseudocode this becomes
Inductive JamesConstruction (A : Type) (a : A) : Type
| epsilon : JamesConstruction A a
| alpha : A -> JamesConstruction A a -> JamesConstruction A a
| delta : forall (x : JamesConstruction A a), x = alpha a x
We can see that is simply the.