3.11 Contractibility


In Lemma 3.3.2 (http://planetmath.org/33merepropositions#Thmprelem1) we observed that a mere proposition which is inhabited must be equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to 𝟏, and it is not hard to see that the converseMathworldPlanetmath also holds. A type with this property is called contractibleMathworldPlanetmath. 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 contrx.

In other words, the type π—‚π—Œπ–’π—ˆπ—‡π—π—‹β’(A) is defined to be

π—‚π—Œπ–’π—ˆπ—‡π—π—‹(A):β‰‘βˆ‘(a:A)∏(x:A)(a=x).

Note that under the usual propositions-as-types reading, we can pronounce π—‚π—Œπ–’π—ˆπ—‡π—π—‹β’(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 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 sentenceMathworldPlanetmath is a continuousPlanetmathPlanetmath/natural one. A more correct way to express connectedness would be βˆ‘(a:A)∏(x:A)βˆ₯a=xβˆ₯; 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 𝟏.

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β‡’3 in Lemma 3.3.2 (http://planetmath.org/33merepropositions#Thmprelem1), while the converse follows since 𝟏 easily has propertyΒ 2. ∎

Lemma 3.11.4.

For any type A, the type isContr⁒(A) is a mere proposition.

Proof.

Suppose given c,cβ€²:π—‚π—Œπ–’π—ˆπ—‡π—π—‹β’(A). We may assume c≑(a,p) and c′≑(aβ€²,pβ€²) for a,aβ€²:A and p:∏(x:A)(a=x) and pβ€²:∏(x:A)(aβ€²=x). By the characterizationMathworldPlanetmath of paths in Ξ£-types, to show c=cβ€² it suffices to exhibit q:a=aβ€² such that q*(p)=pβ€².

We choose q:≑p(aβ€²). For the other equality, by function extensionality we must show that (q*(p))(x)=pβ€²(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⁒\centerdot⁒p⁒(y), since then we would have (q*(p))(x)=p⁒(aβ€²)-1\centerdotp(x)=pβ€²(x). But now we can invoke path inductionMathworldPlanetmath to assume that x≑y and u≑𝗋𝖾𝖿𝗅x. In this case our goal is to show that 𝗋𝖾𝖿𝗅x=p⁒(x)-1⁒\centerdot⁒p⁒(x), which is just the inversion law for paths. ∎

Corollary 3.11.5.

If A is contractible, then so is 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β†’U is a type family such that each P⁒(a) is contractible, then ∏(x:A)P⁒(x) is contractible.

Proof.

By Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2), ∏(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, ∏(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 retractMathworldPlanetmath of A. By definition, a retractionMathworldPlanetmathPlanetmath is a function r:Aβ†’B such that there exists a function s:Bβ†’A, called its sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath, and a homotopyMathworldPlanetmath Ο΅:∏(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 a0:A be the center of contraction. We claim that b0:≑r(a0):B is a center of contraction for B. Let b:B; we need a path b=b0. But we have Ο΅b:r⁒(s⁒(b))=b and π–Όπ—ˆπ—‡π—π—‹s⁒(b):s⁒(b)=a0, so by composition

Ο΅b-1\centerdotr(π–Όπ—ˆπ—‡π—π—‹s⁒(b)):b=r(a0)≑b0.∎

Contractible types may not seem very interesting, since they are all equivalent to 𝟏. One reason the notion is useful is that sometimes a collectionMathworldPlanetmath 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 βˆ‘(x:A)(a=x) is contractible.

Proof.

We choose as center the point (a,𝗋𝖾𝖿𝗅a). Now suppose (x,p):βˆ‘(x:A)(a=x); we must show (a,𝗋𝖾𝖿𝗅a)=(x,p). By the characterization of paths in Ξ£-types, it suffices to exhibit q:a=x such that q*(𝗋𝖾𝖿𝗅a)=p. But we can take q:≑p, in which case q*(𝗋𝖾𝖿𝗅a)=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→U be a type family.

  1. 1.

    If each P⁒(x) is contractible, then βˆ‘(x:A)P⁒(x) is equivalent to A.

  2. 2.

    If A is contractible with center a, then βˆ‘(x:A)P⁒(x) is equivalent to P⁒(a).

Proof.

In the situation ofΒ 1, we show that 𝗉𝗋1:βˆ‘(x:A)P⁒(x)β†’A is an equivalence. For quasi-inverse we define g(x):≑(x,cx) where cx is the center of P⁒(x). The composite 𝗉𝗋1∘g is obviously 𝗂𝖽A, whereas the opposite composite is homotopicMathworldPlanetmath to the identityPlanetmathPlanetmath 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=Ay 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=Ay 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