Contractibility

Definition

A type $X$ is contractible if it contains a point $c:X$, called the center of contraction, such that every other point $x:X$ is connected to $c$ by a path. In Homotopy Type Theory, this is encoded as the type: $\text{isContr}(X)\equiv \Sigma c:X.\Pi x:X.(c=x)$

A contractible type is also referred to as a -2-type.

Properties

Contractibility represents the highest level of triviality in the homotopy level.

• Uniqueness of inhabitants: If a type is contractible, it is equivalent to the unit type $1$.
• Closure under equivalence: If $X\simeq Y$ and $X$ is contractible, then $Y$ is contractible.
• Identity types: If $X$ is contractible, then for any $x,y:X$, the identity type $x=y$ is also contractible, hence all contractible types are propositions.
• Retracts: Any retract of a contractible type is contractible.

Theorems

The relationship between contractibility and other homotopy level is fundamental to the hierarchy of types:

Relation to Mere Propositions

A type $X$ is a mere proposition if and only if for all $x,y:X$, the type $x=y$ is contractible. Alternatively, $X$ is a mere proposition if: $X\to \text{isContr}(X)$

Fiberwise Contractibility

A function $f:A\to B$ is an equivalence if and only if all its fibre are contractible: $\text{isEquiv}(f)\equiv \Pi b:B.\text{isContr}(\Sigma a:A.f(a)=b)$

Examples

• The unit type $1$ is contractible with center of contraction $()$.
• Any singleton type $\Sigma x:A.(a=x)$ is contractible by the path induction principle.
• In unit interval $\mathbb{I}$, the type is contractible to either endpoint.

Related Concepts

• Homotopy Equivalence
• Unit Type
• Identity Type

References

• hott2013-book