The loop space of a pointed type is simply the type of paths from a point to itself i.e. loops.
Given a pointed type the loop space is the type and has basepoint .
The -fold iterated loop space can be defined by induction on : * *
The HoTT book defines a ‘loop space’ in definitions 2.1.7 and 2.1.8:
Definition 2.1.7 A pointed type is a type together with a point , called its basepoint. We write for the type of pointed types in the universe .
Definition 2.1.8 Given a pointed type , we define the loop space of to be the following pointed type:
.
An element of it will be called a loop at . For , the n-fold iterated loop space of a pointed type is defined recursively by:
.An element of it will be called an n-loop or an n-dimensional loop at .
Revision on September 4, 2018 at 13:06:22 by Ali Caglayan. See the history of this page for a list of all contributions to it.