4.4 Contractible fibers
Note that our proofs about and made essential use of the fact that the fibers of an equivalence are contractible. In fact, it turns out that this property is itself a sufficient definition of equivalence.
Definition 4.4.1 (Contractible maps).
A map is contractible if for all , the fiber is contractible.
Thus, the type is defined to be
Note that in §3.11 (http://planetmath.org/311contractibility) we defined what it means for a type to be contractible. Here we are defining what it means for a map to be contractible. Our terminology follows the general homotopy-theoretic practice of saying that a map has a certain property if all of its (homotopy) fibers have that property. Thus, a type is contractible just when the map is contractible. From http://planetmath.org/node/87580Chapter 7 onwards we will also call contractible maps and types -truncated.
For any we have .
Let . We define an inverse mapping by sending each to the center of contraction of the fiber at :
We can thus define the homotopy by mapping to the witness that indeed belongs to the fiber at :
It remains to define and . This of course amounts to giving an element of . By Lemma 4.2.11 (http://planetmath.org/42halfadjointequivalences#Thmprelem5), this is the same as giving for each a path from to in the fiber of over . But this is easy: for any , the type is contractible by assumption, hence such a path must exist. We can construct it explicitly as
It is also easy to see:
For any , the type is a mere proposition.
By Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2), each type is a mere proposition. Thus, by Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2), so is (1). ∎
For any we have .
We have already established a logical equivalence , and both are mere propositions (Lemma 4.4.3 (http://planetmath.org/44contractiblefibers#Thmprelem1),Theorem 4.2.13 (http://planetmath.org/42halfadjointequivalences#Thmprethm3)). Thus, Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2) applies. ∎
Usually, we prove that a function is an equivalence by exhibiting a quasi-inverse, but sometimes this definition is more convenient. For instance, it implies that when proving a function to be an equivalence, we are free to assume that its codomain is inhabited.
If is such that , then is an equivalence.
To show is an equivalence, it suffices to show that is contractible for any . But if , then given any such we have , so that is an equivalence and hence is contractible, as desired. ∎
|Title||4.4 Contractible fibers|