In Lemma 3.3.2 (http://planetmath.org/33merepropositions#Thmprelem1) we observed that a mere proposition which is inhabited must be equivalent to , 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.
In other words, the type is defined to be
Note that under the usual propositions-as-types reading, we can pronounce as “ contains exactly one element”, or more precisely “ contains an element, and every element of is equal to that element”.
We can also pronounce more topologically as “there is a point such that for all there exists a path from to ”. 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 ; see Lemma 7.5.11 (http://planetmath.org/75connectedness#Thmprelem6).
For a type , the following are logically equivalent.
is contractible in the sense of Definition 3.11.1 (http://planetmath.org/311contractibility#Thmpredefn1).
is a mere proposition, and there is a point .
is equivalent to .
If is contractible, then it certainly has a point (the center of contraction), while for any we have ; thus is a mere proposition. Conversely, if we have and is a mere proposition, then for any we have ; thus is contractible. And we showed 23 in Lemma 3.3.2 (http://planetmath.org/33merepropositions#Thmprelem1), while the converse follows since easily has property 2. ∎
For any type , the type is a mere proposition.
Suppose given . We may assume and for and and . By the characterization of paths in -types, to show it suffices to exhibit such that .
We choose . For the other equality, by function extensionality we must show that for any . For this, it will suffice to show that for any and we have , since then we would have . But now we can invoke path induction to assume that and . In this case our goal is to show that , which is just the inversion law for paths. ∎
If is contractible, then so is .
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:
If is a type family such that each is contractible, then is contractible.
By Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2), is a mere proposition since each is. But it also has an element, namely the function sending each to the center of contraction of . Thus by Lemma 3.11.3 (http://planetmath.org/311contractibility#Thmprelem1)2, 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 is equivalent to and is contractible, then so is . More generally, it suffices for to be a retract of . By definition, a retraction is a function such that there exists a function , called its section, and a homotopy ; then we say that is a retract of .
If is a retract of , and is contractible, then so is .
Let be the center of contraction. We claim that is a center of contraction for . Let ; we need a path . But we have and , so by composition
Contractible types may not seem very interesting, since they are all equivalent to . 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.
For any and any , the type is contractible.
We choose as center the point . Now suppose ; we must show . By the characterization of paths in -types, it suffices to exhibit such that . But we can take , in which case 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.
Let be a type family.
If each is contractible, then is equivalent to .
If is contractible with center , then is equivalent to .
In the situation of 1, we show that is an equivalence. For quasi-inverse we define where is the center of . The composite is obviously , whereas the opposite composite is homotopic to the identity by using the contractions of each .
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 -types mentioned in §3.1 (http://planetmath.org/31setsandntypes) downwards one more step.
A type is a mere proposition if and only if for all , the type is contractible.
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 is a mere proposition. But it is also inhabited (since 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 -types. They are the bottom rung of the ladder of -types, and will be the base case of the recursive definition of -types in http://planetmath.org/node/87580Chapter 7.