Showing changes from revision #3 to #4:
Added | Removed | Changed
The James construction on a pointed type . Is the higher inductive type given by
We have an equivalence of types
We can see that is simply the free monoid on . The higher inductive type is recursive which can make it difficult to study. This however can be remedied by defining a sequence of types together with maps such that the type defined as the sequential colimit of is equivalent to .
This is useful as we can study the lower homotopy groups of by studying the lower homotopy groups of the sequential colimit. Which is what allows Brunerie to show .