Homotopy Type Theory
loop space (Rev #2)

The HoTT book defines a ‘loop space’ in definitions 2.1.7 and 2.1.8:

Definition 2.1.7 A pointed type (A,a)(A,a) is a type A:𝒰A\,:\,\mathcal{U} together with a point a:Aa\,:\,A, called its basepoint. We write 𝒰 : (A:𝒰)A\mathcal{U}_\bullet :\equiv \sum_{(A:\mathcal{U})}A for the type of pointed types in the universe 𝒰\mathcal{U}.

Definition 2.1.8 Given a pointed type (A,a)(A,a), we define the loop space of (A,a)(A,a) to be the following pointed type:

Ω(A,a)=((a= Aa),refl a)\Omega(A,a) = ((a =_A a),\,refl_a).

An element of it will be called a loop at aa. For n:n\,:\,\mathbb{N}, the n-fold iterated loop space Ω n(A,a)\Omega^n(A,a) of a pointed type (A,a)(A,a) is defined recursively by:

Ω 0(A,a)=(A,a)\Omega^0(A,a) = (A,a)
Ω n+1(A,a)=Ω n(Ω(A,a))\Omega^{n+1}(A,a) = \Omega^n(\Omega(A,a)).

An element of it will be called an n-loop or an n-dimensional loop at aa.

Revision on May 9, 2014 at 02:02:50 by Alexis Hazell?. See the history of this page for a list of all contributions to it.