4.4 Contractible fibers

Note that our proofs about $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$ and $\mathrm{𝖻𝗂𝗂𝗇𝗏}(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\mathrm{:}A\mathrm{\to }B$ is contractibleif for all $y\mathrm{:}B$, the fiber ${\mathrm{fib}}_f\mathit{}\mathrm{(}y\mathrm{)}$ is contractible.

Thus, the type $\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(f)$ is defined to be

$\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(f)$$:\equiv {\displaystyle \prod _{y:B}}\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}({\mathrm{𝖿𝗂𝖻}}_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 \mathrm{𝟏}$ is contractible.From http://planetmath.org/node/87580Chapter 7 onwards we will also call contractible maps and types $\mathrm{(}\mathrm{-}\mathrm{2}\mathrm{)}$-truncated.

We have already shown in Theorem 4.2.6 (http://planetmath.org/42halfadjointequivalences#Thmprethm2) that $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)\to \mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(f)$.Conversely:

Theorem 4.4.2.

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

Proof.

Let $P:\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(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 {\mathrm{𝗉𝗋}}_1({\mathrm{𝗉𝗋}}_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):\equiv {\mathrm{𝗉𝗋}}_2({\mathrm{𝗉𝗋}}_1(Py))$$

It remains to define $\eta$ and $\tau$. This of course amounts to giving an element of ${\mathrm{𝗋𝖼𝗈𝗁}}_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,{\mathrm{𝗋𝖾𝖿𝗅}}_{fx})$ in the fiber of $f$ over $fx$. But this is easy: for any $x:A$, the type ${\mathrm{𝖿𝗂𝖻}}_f(fx)$is contractible by assumption, hence such a path must exist. We can construct it explicitly as

$${\left({\mathrm{𝗉𝗋}}_2(P(fx))(gfx,ϵ(fx))\right)}^{-1}\left({\mathrm{𝗉𝗋}}_2(P(fx))(x,{\mathrm{𝗋𝖾𝖿𝗅}}_{fx})\right).\mathit{∎}$$

It is also easy to see:

Lemma 4.4.3.

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

Proof.

By Lemma 3.11.4 (http://planetmath.org/311contractibility#Thmprelem2), each type $\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}({\mathrm{𝖿𝗂𝖻}}_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\mathrm{:}A\mathrm{\to }B$ we have $\mathrm{isContr}\mathit{}\mathrm{(}f\mathrm{)}\mathrm{\simeq }\mathrm{ishae}\mathit{}\mathrm{(}f\mathrm{)}$.

Proof.

We have already established a logical equivalence $\mathrm{𝗂𝗌𝖢𝗈𝗇𝗍𝗋}(f)\iff \mathrm{𝗂𝗌𝗁𝖺𝖾}(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\mathrm{:}A\mathrm{\to }B$ is such that $B\mathrm{\to }\mathrm{isequiv}\mathit{}\mathrm{(}f\mathrm{)}$, then $f$ is an equivalence.

Proof.

To show $f$ is an equivalence, it suffices to show that ${\mathrm{𝖿𝗂𝖻}}_f(y)$ is contractible for any $y:B$.But if $e:B\to \mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$, then given any such $y$ we have $e(y):\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$, so that $f$ is an equivalence and hence ${\mathrm{𝖿𝗂𝖻}}_f(y)$ is contractible, as desired.∎