Homotopy Type Theory loop space > history (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)$ is a type $A\,:\,\mathcal{U}$ together with a point $a\,:\,A$, called its basepoint. We write $\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)$, we define the loop space of $(A,a)$ to be the following pointed type:

$\Omega(A,a) = ((a =_A a),\,refl_a)$.

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

$\Omega^0(A,a) = (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 $a$.