**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** =

**propositions as types** +**programs as proofs** +**relation type theory/category theory**

In homotopy type theory, the loop space of a pointed type is simply the type of identifications from a term to itself i.e. loops.

Given a pointed type $(A,\star_A)$ the *loop space type* is the type $\Omega(A,\star_A)\equiv \star_{A} =_{A} \star_{A}$ and has basepoint $refl_{\star A}$.

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

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

Definition 2.1.7Apointed type$(A,a)$ is a type $A\,:\,\mathcal{U}$ together with a point $a\,:\,A$, called itsbasepoint. 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.8Given a pointed type $(A,a)$, we define theloop spaceof $(A,a)$ to be the following pointed type:$\Omega(A,a) = ((a =_A a),\,refl_a)$.

An element of it will be called a

loopat $a$. For $n\,:\,\mathbb{N}$, then-folditerated 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-loopor ann-dimensionalloopat $a$.

Last revised on June 9, 2022 at 16:49:15. See the history of this page for a list of all contributions to it.