# 4.4 Contractible fibers

Note that our proofs about $\mathsf{ishae}(f)$ and $\mathsf{biinv}(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\to B$ is contractible if for all $y:B$, the fiber ${\mathsf{fib}}_{f}(y)$ is contractible.

Thus, the type $\mathsf{isContr}(f)$ is defined to be

 $\displaystyle\mathsf{isContr}(f)$ $\displaystyle:\!\!\equiv\mathchoice{\prod_{y:B}\,}{\mathchoice{{\textstyle% \prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{% \textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{% \mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y% :B)}}}\mathsf{isContr}({\mathsf{fib}}_{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\to\mathbf{1}$ 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 $\mathsf{ishae}(f)\to\mathsf{isContr}(f)$. Conversely:

###### Theorem 4.4.2.

For any $f:A\to B$ we have ${\mathsf{isContr}(f)}\to{\mathsf{ishae}(f)}$.

###### Proof.

Let $P:\mathsf{isContr}(f)$. We define an inverse mapping $g:B\to A$ by sending each $y:B$ to the center of contraction of the fiber at $y$:

 $g(y):\!\!\equiv\mathsf{pr}_{1}(\mathsf{pr}_{1}(Py))$

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

 $\epsilon(y):\!\!\equiv\mathsf{pr}_{2}(\mathsf{pr}_{1}(Py))$

It remains to define $\eta$ and $\tau$. This of course amounts to giving an element of $\mathsf{rcoh}_{f}(g,\epsilon)$. By Lemma 4.2.11 (http://planetmath.org/42halfadjointequivalences#Thmprelem5), this is the same as giving for each $x:A$ a path from $(gfx,\epsilon(fx))$ to $(x,\mathsf{refl}_{fx})$ in the fiber of $f$ over $fx$. But this is easy: for any $x:A$, the type ${\mathsf{fib}}_{f}(fx)$ is contractible by assumption, hence such a path must exist. We can construct it explicitly as

 $\mathord{{\big{(}\mathsf{pr}_{2}(P(fx))(gfx,\epsilon(fx))\big{)}}^{-1}}% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}\big{(}\mathsf{pr}_{2}(P(fx))(x,\mathsf{refl}_{fx})\big{)}.\qed$

It is also easy to see:

###### Lemma 4.4.3.

For any $f$, the type $\mathsf{isContr}(f)$ is a mere proposition.

###### Proof.

By Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2), each type $\mathsf{isContr}({\mathsf{fib}}_{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\to B$ we have $\mathsf{isContr}(f)\simeq\mathsf{ishae}(f)$.

###### Proof.

We have already established a logical equivalence ${\mathsf{isContr}(f)}\Leftrightarrow{\mathsf{ishae}(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\to B$ is such that $B\to\mathsf{isequiv}(f)$, then $f$ is an equivalence.

###### Proof.

To show $f$ is an equivalence, it suffices to show that ${\mathsf{fib}}_{f}(y)$ is contractible for any $y:B$. But if $e:B\to\mathsf{isequiv}(f)$, then given any such $y$ we have $e(y):\mathsf{isequiv}(f)$, so that $f$ is an equivalence and hence ${\mathsf{fib}}_{f}(y)$ is contractible, as desired. ∎

Title 4.4 Contractible fibers
\metatable