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 contractibleMathworldPlanetmath. 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 (homotopyMathworldPlanetmath) 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).


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:


We can thus define the homotopy ϡ by mapping y to the witness that g⁒(y) indeed belongs to the fiber at y:


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 (g⁒f⁒x,ϡ⁒(f⁒x)) to (x,𝗋𝖾𝖿𝗅f⁒x) in the fiber of f over f⁒x. But this is easy: for any x:A, the type 𝖿𝗂𝖻f⁒(f⁒x) is contractible by assumptionPlanetmathPlanetmath, hence such a path must exist. We can construct it explicitly as


It is also easy to see:

Lemma 4.4.3.

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


By Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2), each type π—‚π—Œπ–’π—ˆπ—‡π—π—‹β’(𝖿𝗂𝖻f⁒(y)) is a mere proposition. Thus, by Example 3.6.2 (http://planetmath.org/36thelogicofmerepropositions#Thmpreeg2), so isΒ (1). ∎

Theorem 4.4.4.

For any f:Aβ†’B we have isContr⁒(f)≃ishae⁒(f).


We have already established a logical equivalence π—‚π—Œπ–’π—ˆπ—‡π—π—‹β’(f)β‡”π—‚π—Œπ—π–Ίπ–Ύβ’(f), 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 f:Aβ†’B is such that Bβ†’isequiv⁒(f), then f is an equivalence.


To show f is an equivalence, it suffices to show that 𝖿𝗂𝖻f⁒(y) is contractible for any y:B. But if e:Bβ†’π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—β’(f), then given any such y we have e⁒(y):π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—β’(f), so that f is an equivalence and hence 𝖿𝗂𝖻f⁒(y) is contractible, as desired. ∎

Title 4.4 Contractible fibers