nLab loop type

Disambiguation

Similar to path types, there are a few different types which can be called loop types or loop space types in dependent type theory.

• The identity type $x =_A x$ for type $A$ and element $x:A$, which is the type of self-identifications of $x:A$ or the based loop space type $\Omega_A(x)$ of $x:A$;

• The type of pointed type homomorphisms

  $$S^1 \to_{*} A \equiv \sum_{f:S^1 \to A} f(\mathrm{base}) =_A x$$

  from the circle type $S^1$ to a type $A$ with element $x:A$ - this parallels the topological definition of loop spaces as continuous functions out of the unit circle to a pointed topological space;

The categorical semantics of loop types in any of the above forms is the loop space object.

There are also other types which could be called the free loop type or free loop space type:

• The dependent sum type $\sum_{x:A} x =_A x$ for type $A$, which is the type of all self-identifications in $A$;

• The function type $S^1 \to A$ from the circle type $S^1$ to a type $A$ - this parallels the topological definition of free loop spaces as continuous functions out of the unit circle to a topological space;

The categorical semantics of free loop types in any of the above forms is the free loop space object.

Related concepts

• path type

category: disambiguation