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.

$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 $\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 retraction is a function $r:A\to B$ such that there exists a function $s:B\to A$ , called its section, 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.

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.

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