Showing changes from revision #7 to #8:
Added | Removed | Changed
The James construction on a pointed type . Is the higher inductive type given by
We have an equivalence of types if is 0-connected.
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 .
Revision on September 4, 2018 at 13:38:31 by Ali Caglayan. See the history of this page for a list of all contributions to it.