nLab loop space type

Idea

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.

Definition

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.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$.

Properties

The axiom K on a type states that for every element $a:A$, reflexivity $\mathrm{refl}_A(a)$ is the center of contraction of the loop space type of $a$.

Pointed connected groupoids

Given a pointed connected groupoid $(A, a)$, the loop space type $\Omega(A, a)$ is a group. In fact, for every group $G$, one could form the delooping of $G$ as a higher inductive type generated by

• a type $B(G)$,
• an element $*:B(G)$,
• elements $a:G \vdash h(a):\Omega(B(G), *)$,
• identities $a:G, b:G \vdash \mathrm{isGrpHom}(h, a, b):h(a \cdot b) =_{\Omega(B(G), *)} \mathrm{comp}_{*, *, *}(h(a), h(b))$
• a witness $p:\mathrm{isGrpd}(B(G))$

Related entries

• pointed type

• identity type

• autoequivalence type

References

• Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)