[[the HoTT book|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$.