3.11 Contractibility

In Lemma 3.3.2 (http://planetmath.org/33merepropositions#Thmprelem1) we observed that a mere proposition which is inhabited must be equivalent to $\mathrm{𝟏}$,and it is not hard to see that the converse also holds.A type with this property is called contractible.Another equivalent definition of contractibility, which is also sometimes convenient, is the following.

Definition 3.11.1.

A type $A$ is contractible,or a singleton,if there is $a\mathrm{:}A$, called the center of contraction,such that $a\mathrm{=}x$ for all $x\mathrm{:}A$.We denote the specified path $a\mathrm{=}x$ by ${\mathrm{contr}}_x$.

In other words, the type $\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(A)$ is defined to be

$$\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(A):\equiv \sum _{(a:A)}\prod _{(x:A)}(a=x).$$

Note that under the usual propositions-as-types reading, we can pronounce $\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(A)$ as “$A$ contains exactly one element”, or more precisely “$A$ contains an element, and every element of $A$ is equal to that element”.

Remark 3.11.2.

We can also pronounce $\mathrm{isContr}\mathit{}\mathrm{(}A\mathrm{)}$ more topologically as “there is a point $a\mathrm{:}A$ such that for all $x\mathrm{:}A$ there exists a path from $a$ to $x$”.Note that to a classical ear, this sounds like a definition of connectedness rather than contractibility.The point is that the meaning of “there exists” in this sentence is a continuous/natural one.A more correct way to express connectedness would be ${\mathrm{\sum }}_{\mathrm{(}a\mathrm{:}A\mathrm{)}}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathrm{\parallel }a\mathrm{=}x\mathrm{\parallel }$; see Lemma 7.5.11 (http://planetmath.org/75connectedness#Thmprelem6).

Lemma 3.11.3.

For a type $A$, the following are logically equivalent.

1. $A$ is contractible in the sense of Definition 3.11.1 (http://planetmath.org/311contractibility#Thmpredefn1).

2. $A$ is a mere proposition, and there is a point $a:A$.

3. $A$ is equivalent to $\mathrm{𝟏}$.

Proof.

If $A$ is contractible, then it certainly has a point $a:A$ (the center of contraction), while for any $x,y:A$ we have $x=a=y$; thus $A$ is a mere proposition.Conversely, if we have $a:A$ and $A$ is a mere proposition, then for any $x:A$ we have $x=a$; thus $A$ is contractible.And we showed 2$\Rightarrow$3 in Lemma 3.3.2 (http://planetmath.org/33merepropositions#Thmprelem1), while the converse follows since $\mathrm{𝟏}$ easily has property 2.∎

Lemma 3.11.4.

For any type $A$, the type $\mathrm{isContr}\mathit{}\mathrm{(}A\mathrm{)}$ is a mere proposition.

Proof.

Suppose given $c,c^{\prime }:\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(A)$.We may assume $c\equiv (a,p)$ and $c^{\prime }\equiv (a^{\prime },p^{\prime })$ for $a,a^{\prime }:A$ and $p:{\prod }_{(x:A)}(a=x)$ and $p^{\prime }:{\prod }_{(x:A)}(a^{\prime }=x)$.By the characterization of paths in $\mathrm{\Sigma }$-types, to show $c=c^{\prime }$ it suffices to exhibit $q:a=a^{\prime }$ such that $q_{*}\left(p\right)=p^{\prime }$.

We choose $q:\equiv p(a^{\prime })$.For the other equality, by function extensionality we must show that $(q_{*}\left(p\right))(x)=p^{\prime }(x)$ for any $x:A$.For this, it will suffice to show that for any $x,y:A$ and $u:x=y$ we have $u=p{(x)}^{-1}p(y)$, since then we would have $(q_{*}\left(p\right))(x)=p{(a^{\prime })}^{-1}p(x)=p^{\prime }(x)$.But now we can invoke path induction to assume that $x\equiv y$ and $u\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_x$.In this case our goal is to show that ${\mathrm{𝗋𝖾𝖿𝗅}}_x=p{(x)}^{-1}p(x)$, which is just the inversion law for paths.∎

Corollary 3.11.5.

If $A$ is contractible, then so is $\mathrm{isContr}\mathit{}\mathrm{(}A\mathrm{)}$.

Proof.

By Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2) and Lemma 3.11.3 (http://planetmath.org/311contractibility#Thmprelem1)2.∎

Like mere propositions, contractible types are preserved by many type constructors.For instance, we have:

Lemma 3.11.6.

If $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ is a type family such that each $P\mathit{}\mathrm{(}a\mathrm{)}$ is contractible, then ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$ is contractible.

Proof.

By Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2), ${\prod }_{(x:A)}P(x)$ is a mere proposition since each $P(x)$ is.But it also has an element, namely the function sending each $x:A$ to the center of contraction of $P(x)$.Thus by Lemma 3.11.3 (http://planetmath.org/311contractibility#Thmprelem1)2, ${\prod }_{(x:A)}P(x)$ is contractible.∎

(In fact, the statement of Lemma 3.11.6 (http://planetmath.org/311contractibility#Thmprelem3) is equivalent to the function extensionality axiom.See §4.9 (http://planetmath.org/49univalenceimpliesfunctionextensionality).)

Of course, if $A$ is equivalent to $B$ and $A$ is contractible, then so is $B$.More generally, it suffices for $B$ to be a retract of $A$.By definition, a retractionis a function $r:A\to B$ such that there exists a function $s:B\to A$, called its section,and a homotopy $ϵ:{\prod }_{(y:B)}(r(s(y))=y)$; then we say that $B$ is a retractof $A$.

Lemma 3.11.7.

If $B$ is a retract of $A$, and $A$ is contractible, then so is $B$.

Proof.

Let $a_0:A$ be the center of contraction.We claim that $b_0:\equiv r(a_0):B$ is a center of contraction for $B$.Let $b:B$; we need a path $b=b_0$.But we have ${ϵ}_b:r(s(b))=b$ and ${\mathrm{𝖼𝗈𝗇𝗍𝗋}}_{s(b)}:s(b)=a_0$, so by composition

$$ϵ_b{}^{-1}r\left({\mathrm{𝖼𝗈𝗇𝗍𝗋}}_{s(b)}\right):b=r(a_0)\equiv b_0.\mathit{∎}$$

Contractible types may not seem very interesting, since they are all equivalent to $\mathrm{𝟏}$.One reason the notion is useful is that sometimes a collection of individually nontrivial data will collectively form a contractible type.An important example is the space of paths with one free endpoint.As we will see in §5.8 (http://planetmath.org/58identitytypesandidentitysystems), this fact essentiallyencapsulates the based path induction principle for identity types.

Lemma 3.11.8.

For any $A$ and any $a\mathrm{:}A$, the type ${\mathrm{\sum }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathrm{(}a\mathrm{=}x\mathrm{)}$ is contractible.

Proof.

We choose as center the point $(a,{\mathrm{𝗋𝖾𝖿𝗅}}_a)$.Now suppose $(x,p):{\sum }_{(x:A)}(a=x)$; we must show $(a,{\mathrm{𝗋𝖾𝖿𝗅}}_a)=(x,p)$.By the characterization of paths in $\mathrm{\Sigma }$-types, it suffices to exhibit $q:a=x$ such that $q_{*}\left({\mathrm{𝗋𝖾𝖿𝗅}}_a\right)=p$.But we can take $q:\equiv p$, in which case $q_{*}\left({\mathrm{𝗋𝖾𝖿𝗅}}_a\right)=p$ follows from the characterization of transport in path types.∎

When this happens, it can allow us to simplify a complicated construction up to equivalence, using the informal principle that contractible data can be freely ignored.This principle consists of many lemmas, most of which we leave to the reader; the following is an example.

Lemma 3.11.9.

Let $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ be a type family.

1. If each $P(x)$ is contractible, then ${\sum }_{(x:A)}P(x)$ is equivalent to $A$.

2. If $A$ is contractible with center $a$, then ${\sum }_{(x:A)}P(x)$ is equivalent to $P(a)$.

Proof.

In the situation of 1, we show that ${\mathrm{𝗉𝗋}}_1:{\sum }_{(x:A)}P(x)\to A$ is an equivalence.For quasi-inverse we define $g(x):\equiv (x,c_x)$ where $c_x$ is the center of $P(x)$.The composite ${\mathrm{𝗉𝗋}}_1\circ g$ is obviously ${\mathrm{𝗂𝖽}}_A$, whereas the opposite composite is homotopic to the identity by using the contractions of each $P(x)$.

We leave the proof of 2 to the reader (see http://planetmath.org/node/87806Exercise 3.20).∎

Another reason contractible types are interesting is that they extend the ladder of $n$-types mentioned in §3.1 (http://planetmath.org/31setsandntypes) downwards one more step.

Lemma 3.11.10.

A type $A$ is a mere proposition if and only if for all $x\mathrm{,}y\mathrm{:}A$, the type $x{\mathrm{=}}_{A}y$ is contractible.

Proof.

For “if”, we simply observe that any contractible type is inhabited.For “only if”, we observed in §3.3 (http://planetmath.org/33merepropositions) that every mere proposition is a set, so that each type $x{=}_{A}y$ is a mere proposition.But it is also inhabited (since $A$ is a mere proposition), and hence by Lemma 3.11.3 (http://planetmath.org/311contractibility#Thmprelem1)2 it is contractible.∎

Thus, contractible types may also be called $(-2)$-types.They are the bottom rung of the ladder of $n$-types, and will be the base case of the recursive definition of $n$-types in http://planetmath.org/node/87580Chapter 7.