Homotopy Type Theory
loop space


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 (A, A)(A,\star_A) the loop space is the type Ω(A, A) A= A A\Omega(A,\star_A)\equiv \star_{A} =_{A} \star_{A} and has basepoint refl Arefl_{\star A}.

The nn-fold iterated loop space Ω n(A, A)\Omega^n(A,\star_A) can be defined by induction on nn: * Ω 0(A, A)=(A, A)\Omega^0(A,\star_A)=(A,\star_A) * Ω n+1(A, A)=Ω n(Ω(A, A))\Omega^{n+1}(A,\star_A)=\Omega^n(\Omega(A,\star_A))


HoTT book

category: homotopy theory

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.

Last revised on September 4, 2018 at 09:06:22. See the history of this page for a list of all contributions to it.