# 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 $\mathbf{1}$, 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:A$, called the center of contraction, such that $a=x$ for all $x:A$. We denote the specified path $a=x$ by $\mathsf{contr}_{x}$.

In other words, the type $\mathsf{isContr}(A)$ is defined to be

 $\mathsf{isContr}(A):\!\!\equiv\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{% \textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{% \mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}% }}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:% A)}}}\mathchoice{\prod_{(x:A)}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{% (x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(a=x).$

Note that under the usual propositions-as-types reading, we can pronounce $\mathsf{isContr}(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 $\mathsf{isContr}(A)$ more topologically as “there is a point $a:A$ such that for all $x: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 $\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:A)}% }{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{(a:% A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_{(a:A)}}}{\sum_{% (a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice{\prod_{(x:A)}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}\mathopen{}\left\|a=x\right\|\mathclose{}$; see Lemma 7.5.11 (http://planetmath.org/75connectedness#Thmprelem6).

###### Lemma 3.11.3.

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

1. 1.

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

2. 2.

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

3. 3.

$A$ is equivalent to $\mathbf{1}$.

###### 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 $\mathbf{1}$ easily has property 2. ∎

###### Lemma 3.11.4.

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

###### Proof.

Suppose given $c,c^{\prime}:\mathsf{isContr}(A)$. We may assume $c\equiv(a,p)$ and $c^{\prime}\equiv(a^{\prime},p^{\prime})$ for $a,a^{\prime}:A$ and $p:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(a=x)$ and $p^{\prime}:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(a^{\prime}=x)$. By the characterization of paths in $\Sigma$-types, to show $c=c^{\prime}$ it suffices to exhibit $q:a=a^{\prime}$ such that ${q}_{*}\mathopen{}\left({p}\right)\mathclose{}=p^{\prime}$.

We choose $q:\!\!\equiv p(a^{\prime})$. For the other equality, by function extensionality we must show that $({q}_{*}\mathopen{}\left({p}\right)\mathclose{})(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=\mathord{{p(x)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}p(y)$, since then we would have $({q}_{*}\mathopen{}\left({p}\right)\mathclose{})(x)=\mathord{{p(a^{\prime})}^{% -1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}p(x)=p^{\prime}(x)$. But now we can invoke path induction to assume that $x\equiv y$ and $u\equiv\mathsf{refl}_{x}$. In this case our goal is to show that $\mathsf{refl}_{x}=\mathord{{p(x)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p(x)$, which is just the inversion law for paths. ∎

###### Corollary 3.11.5.

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

###### 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:A\to\mathcal{U}$ is a type family such that each $P(a)$ is contractible, then $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)$ is contractible.

###### Proof.

By Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2), $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\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, $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\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 is a function $r:A\to B$ such that there exists a function $s:B\to A$, called its , and a homotopy $\epsilon:\mathchoice{\prod_{y:B}\,}{\mathchoice{{\textstyle\prod_{(y:B)}}}{% \prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{\textstyle\prod_{(y% :B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{\textstyle% \prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}(r(s(y))=y)$; then we say that $B$ is a retract of $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 $\epsilon_{b}:r(s(b))=b$ and $\mathsf{contr}_{s(b)}:s(b)=a_{0}$, so by composition

 $\mathord{{\epsilon_{b}}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}{r}\mathopen{}\left({\mathsf{% contr}_{s(b)}}\right)\mathclose{}:b=r(a_{0})\equiv b_{0}.\qed$

Contractible types may not seem very interesting, since they are all equivalent to $\mathbf{1}$. 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 essentially encapsulates the based path induction principle for identity types.

###### Lemma 3.11.8.

For any $A$ and any $a:A$, the type $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}(a=x)$ is contractible.

###### Proof.

We choose as center the point $(a,\mathsf{refl}_{a})$. Now suppose $(x,p):\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_% {(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}(a=x)$; we must show $(a,\mathsf{refl}_{a})=(x,p)$. By the characterization of paths in $\Sigma$-types, it suffices to exhibit $q:a=x$ such that ${q}_{*}\mathopen{}\left({\mathsf{refl}_{a}}\right)\mathclose{}=p$. But we can take $q:\!\!\equiv p$, in which case ${q}_{*}\mathopen{}\left({\mathsf{refl}_{a}}\right)\mathclose{}=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:A\to\mathcal{U}$ be a type family.

1. 1.

If each $P(x)$ is contractible, then $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$ is equivalent to $A$.

2. 2.

If $A$ is contractible with center $a$, then $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$ is equivalent to $P(a)$.

###### Proof.

In the situation of 1, we show that $\mathsf{pr}_{1}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}% }{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\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 $\mathsf{pr}_{1}\circ g$ is obviously $\mathsf{id}_{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,y:A$, the type $x=_{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.

Title 3.11 Contractibility
\metatable