Singleton Type

Definition

A singleton type (sometimes referred to as a based path space) centered at $a:A$ is the dependent pair type: $\Sigma x:A.(a=x)$ This type consists of pairs $(x,p)$ where $x$ is an element of $A$ and $p$ is a path from $a$ to $x$.

Contractibility

The most critical property of the singleton type is that it is contractibile for any $a:A$. This is expressed by the term: $\text{isContr}(\Sigma x:A.a=x)$ The center of contraction is the pair $(a,{\text{refl}}_a)$, where ${\text{refl}}_a$ is the constant path at $a$.

Proof via Path Induction

The contractibility of the singleton type is logically equivalent to the path induction principle (also known as $J$). To prove $\Pi z:(\Sigma x:A.a=x).(a,{\text{refl}}_a)=z$, we apply path induction:

• Let $z$ be a pair $(x,p)$.
• Path induction allows us to assume $x$ is $a$ and $p$ is ${\text{refl}}_a$.
• Under this assumption, the goal becomes $(a,{\text{refl}}_a)=(a,{\text{refl}}_a)$, which is satisfied by ${\text{refl}}_{(a,{\text{refl}}_a)}$.

Notation

In some contexts, the singleton type is denoted as:

• ${\text{path}}_a$
• $P_{a}A$ (the space of paths in $A$ starting at $a$)

Properties

• The singleton type can be viewed as the Fibrancy (HoTT) of the identity map or a projection.
• In the context of the univalence axiom, the singleton type over the universe $U$ for a type $A$, defined as $\Sigma X:U.(A\simeq X)$, is also contractible.

Related Concepts

• Identity Type
• Contractible
• Identity Type
• Fibrancy (HoTT)

References

• hott2013-book