4.4 Contractible fibers
Note that our proofs about ππππΊπΎ(f) and π»ππππ(f) 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 f:AβB is contractible if for all y:B, the fiber fibf(y) is contractible.
Thus, the type πππ’ππππ(f) is defined to be
πππ’ππππ(f) | :β‘βy:Bπππ’ππππ(πΏππ»f(y)) | (1) |
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 A is contractible just when the map Aβπ is contractible.
From http://planetmath.org/node/87580Chapter 7 onwards we will also call contractible maps and types (-2)-truncated.
We have already shown in Theorem 4.2.6 (http://planetmath.org/42halfadjointequivalences#Thmprethm2) that ππππΊπΎ(f)βπππ’ππππ(f). Conversely:
Theorem 4.4.2.
For any f:AβB we have isContr(f)βishae(f).
Proof.
Let P:πππ’ππππ(f). We define an inverse mapping g:BβA by sending each y:B to the center of contraction of the fiber at y:
g(y):β‘ππ1(ππ1(Py)) |
We can thus define the homotopy Ο΅ by mapping y to the witness that g(y) indeed belongs to the fiber at y:
Ο΅(y):β‘ππ2(ππ1(Py)) |
It remains to define Ξ· and Ο. This of course amounts to giving an element of ππΌππf(g,Ο΅). By Lemma 4.2.11 (http://planetmath.org/42halfadjointequivalences#Thmprelem5), this is the same as giving for each x:A a path from (gfx,Ο΅(fx)) to (x,ππΎπΏπ
fx) in the fiber of f over fx. But this is easy: for any x:A, the type πΏππ»f(fx)
is contractible by assumption, hence such a path must exist. We can construct it explicitly as
(ππ2(P(fx))(gfx,Ο΅(fx)))-1\centerdot(ππ2(P(fx))(x,ππΎπΏπ fx)).β |
It is also easy to see:
Lemma 4.4.3.
For any , the type is a mere proposition.
Proof.
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). β
Theorem 4.4.4.
For any we have .
Proof.
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.
Corollary 4.4.5.
If is such that , then is an equivalence.
Proof.
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 |
---|---|
\metatable |