4.7 Closure properties of equivalences

We have already seen in Lemma 2.4.12 (http://planetmath.org/http://planetmath.org/24homotopiesandequivalences#Thmprelem3) that equivalences are closed under composition. Furthermore, we have:

Theorem 4.7.1 (The 2-out-of-3 property).

Suppose $f\mathrm{:}A\mathrm{\to }B$ and $g\mathrm{:}B\mathrm{\to }C$. If any two of $f$, $g$, and $g\mathrm{\circ }f$ are equivalences, so is the third.

Proof.

If $g\circ f$ and $g$ are equivalences, then ${(g\circ f)}^{-1}\circ g$ is a quasi-inverse to $f$. On the one hand, we have ${(g\circ f)}^{-1}\circ g\circ f\sim {\mathrm{𝗂𝖽}}_A$, while on the other we have

$f\circ {(g\circ f)}^{-1}\circ g$ $\sim g^{-1}\circ g\circ f\circ {(g\circ f)}^{-1}\circ g$

$\sim g^{-1}\circ g$

$\sim {\mathrm{𝗂𝖽}}_B.$

Similarly, if $g\circ f$ and $f$ are equivalences, then $f\circ {(g\circ f)}^{-1}$ is a quasi-inverse to $g$. ∎

This is a standard closure condition on equivalences from homotopy theory. Also well-known is that they are closed under retracts, in the following sense.

Definition 4.7.2.

A function $g\mathrm{:}A\mathrm{\to }B$ is said to be a retract of a function $f\mathrm{:}X\mathrm{\to }Y$ if there is a diagram

HoTT_fig_4.7.1.png

for which there are

1. a homotopy $R:r\circ s\sim {\mathrm{𝗂𝖽}}_A$.

2. a homotopy $R^{\prime }:r^{\prime }\circ s^{\prime }\sim {\mathrm{𝗂𝖽}}_B$.

3. a homotopy $L:f\circ s\sim s^{\prime }\circ g$.

4. a homotopy $K:g\circ r\sim r^{\prime }\circ f$.

5. for every $a:A$, a path $H(a)$ witnessing the commutativity of the square

   HoTT_fig_4.7.2.png

Recall that in §3.11 (http://planetmath.org/311contractibility) we defined what it means for a type to be a retract of another. This is a special case of the above definition where $B$ and $Y$ are $\mathrm{𝟏}$. Conversely, just as with contractibility, retractions of maps induce retractions of their fibers.

Lemma 4.7.3.

If a function $g\mathrm{:}A\mathrm{\to }B$ is a retract of a function $f\mathrm{:}X\mathrm{\to }Y$, then ${\mathrm{fib}}_g\mathit{}\mathrm{(}b\mathrm{)}$ is a retract of ${\mathrm{fib}}_f\mathit{}\mathrm{(}{s}^{\mathrm{\prime }}\mathit{}\mathrm{(}b\mathrm{)}\mathrm{)}$ for every $b\mathrm{:}B$, where $s^{\mathrm{\prime }}\mathrm{:}B\mathrm{\to }Y$ is as in Definition 4.7.2 (http://planetmath.org/47closurepropertiesofequivalences#Thmpredefn1).

Proof.

Suppose that $g:A\to B$ is a retract of $f:X\to Y$. Then for any $b:B$ we have the functions

${\phi }_b$ $:{\mathrm{𝖿𝗂𝖻}}_g(b)\to {\mathrm{𝖿𝗂𝖻}}_f(s^{\prime }(b)),$ ${\phi }_b(a,p)$ $:\equiv (s(a),L(a)s^{\prime }(p)),$

${\psi }_b$ $:{\mathrm{𝖿𝗂𝖻}}_f(s^{\prime }(b))\to {\mathrm{𝖿𝗂𝖻}}_g(b),$ ${\psi }_b(x,q)$ $:\equiv (r(x),K(x)r^{\prime }(q)R^{\prime }(b)).$

Then we have ${\psi }_b({\phi }_b(a,p))\equiv (r(s(a)),K(s(a))r^{\prime }(L(a)s^{\prime }(p))R^{\prime }(b))$. We claim ${\psi }_b$ is a retraction with section ${\phi }_b$ for all $b:B$, which is to say that for all $(a,p):{\mathrm{𝖿𝗂𝖻}}_g(b)$ we have ${\psi }_b({\phi }_b(a,p))=(a,p)$. In other words, we want to show

$$\prod _{(b:B)}\prod _{(a:A)}\prod _{(p:g(a)=b)}{\psi }_b({\phi }_b(a,p))=(a,p).$$

By reordering the first two $\mathrm{\Pi }$s and applying a version of Lemma 3.11.9 (http://planetmath.org/311contractibility#Thmprelem6), this is equivalent to

$$\prod _{a:A}{\psi }_{g(a)}({\phi }_{g(a)}(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{g(a)}))=(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{g(a)}).$$

For any $a$, by Theorem 2.7.2 (http://planetmath.org/27sigmatypes#Thmprethm1), this equality of pairs is equivalent to a pair of equalities. The first components are equal by $R(a):r(s(a))=a$, so we need only show

$$R{(a)}_{*}\left(K(s(a))r^{\prime }(L(a))R^{\prime }(g(a))\right)={\mathrm{𝗋𝖾𝖿𝗅}}_{g(a)}.$$

But this transportation computes as $g{(R(a))}^{-1}K(s(a))r^{\prime }(L(a))R^{\prime }(g(a))$, so the required path is given by $H(a)$. ∎

Theorem 4.7.4.

If $g$ is a retract of an equivalence $f$, then $g$ is also an equivalence.

Proof.

By Lemma 4.7.3 (http://planetmath.org/47closurepropertiesofequivalences#Thmprelem1), every fiber of $g$ is a retract of a fiber of $f$. Thus, by Lemma 3.11.7 (http://planetmath.org/311contractibility#Thmprelem4), if the latter are all contractible, so are the former. ∎

Finally, we show that fiberwise equivalences can be characterized in terms of equivalences of total spaces. To explain the terminology, recall from §2.3 (http://planetmath.org/23typefamiliesarefibrations) that a type family $P:A\to 𝒰$ can be viewed as a fibration over $A$ with total space ${\sum }_{(x:A)}P(x)$, the fibration being is the projection ${\mathrm{𝗉𝗋}}_1:{\sum }_{(x:A)}P(x)\to A$. From this point of view, given two type families $P,Q:A\to 𝒰$, we may refer to a function $f:{\prod }_{(x:A)}(P(x)\to Q(x))$ as a fiberwise map or a fiberwise transformation. Such a map induces a function on total spaces:

Definition 4.7.5.

Given type families $P\mathrm{,}Q\mathrm{:}A\mathrm{\to }\mathrm{U}$ and a map $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}\mathrm{\to }Q\mathit{}\mathrm{(}x\mathrm{)}$, we define

$$\mathrm{𝗍𝗈𝗍𝖺𝗅}(f):\equiv \lambda w.({\mathrm{𝗉𝗋}}_{1}w,f({\mathrm{𝗉𝗋}}_{1}w,{\mathrm{𝗉𝗋}}_{2}w)):\sum _{x:A}P(x)\to \sum _{x:A}Q(x).$$

Theorem 4.7.6.

Suppose that $f$ is a fiberwise transformation between families $P$ and $Q$ over a type $A$ and let $x\mathrm{:}A$ and $v\mathrm{:}Q\mathit{}\mathrm{(}x\mathrm{)}$. Then we have an equivalence

$${\mathrm{𝖿𝗂𝖻}}_{\mathrm{𝗍𝗈𝗍𝖺𝗅}(f)}((x,v))\simeq {\mathrm{𝖿𝗂𝖻}}_{f(x)}(v).$$

Proof.

We calculate:

${\mathrm{𝖿𝗂𝖻}}_{\mathrm{𝗍𝗈𝗍𝖺𝗅}(f)}((x,v))$ $\equiv {\displaystyle \sum _{w:{\sum }_{(x:A)}P(x)}}({\mathrm{𝗉𝗋}}_{1}w,f({\mathrm{𝗉𝗋}}_{1}w,{\mathrm{𝗉𝗋}}_{2}w))=(x,v)$

$\simeq {\displaystyle \sum _{(a:A)}}{\displaystyle \sum _{(u:P(a))}}(a,f(a,u))=(x,v)$ (by http://planetmath.org/node/87641Exercise 2.10)

$\simeq {\displaystyle \sum _{(a:A)}}{\displaystyle \sum _{(u:P(a))}}{\displaystyle \sum _{(p:a=x)}}{p}_{*}\left(f(a,u)\right)=v$ (by Theorem 0.1 (http://planetmath.org/27sigmatypes0.Thmthm1))

$\simeq {\displaystyle \sum _{(a:A)}}{\displaystyle \sum _{(p:a=x)}}{\displaystyle \sum _{(u:P(a))}}{p}_{*}\left(f(a,u)\right)=v$

$\simeq {\displaystyle \sum _{u:P(x)}}f(x,u)=v$ ($*$)

$\equiv {\mathrm{𝖿𝗂𝖻}}_{f(x)}(v).$

The equivalence (($*$) ‣ 4.7 Closure properties of equivalences) follows from Lemma 3.11.9 (http://planetmath.org/311contractibility#Thmprelem6),Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5),http://planetmath.org/node/87641Exercise 2.10. ∎

We say that a fiberwise transformation $f:{\prod }_{(x:A)}P(x)\to Q(x)$ is a fiberwise equivalence if each $f(x):P(x)\to Q(x)$ is an equivalence.

Theorem 4.7.7.

Suppose that $f$ is a fiberwise transformation between families $P$ and $Q$ over a type $A$. Then $f$ is a fiberwise equivalence if and only if $\mathrm{total}\mathit{}\mathrm{(}f\mathrm{)}$ is an equivalence.

Proof.

Let $f$, $P$, $Q$ and $A$ be as in the statement of the theorem. By Theorem 4.7.6 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm3) it follows for all $x:A$ and $v:Q(x)$ that ${\mathrm{𝖿𝗂𝖻}}_{\mathrm{𝗍𝗈𝗍𝖺𝗅}(f)}((x,v))$ is contractible if and only if ${\mathrm{𝖿𝗂𝖻}}_{f(x)}(v)$ is contractible. Thus, ${\mathrm{𝖿𝗂𝖻}}_{\mathrm{𝗍𝗈𝗍𝖺𝗅}(f)}(w)$ is contractible for all $w:{\sum }_{(x:A)}Q(x)$ if and only if ${\mathrm{𝖿𝗂𝖻}}_{f(x)}(v)$ is contractible for all $x:A$ and $v:Q(x)$. ∎

Title	4.7 Closure properties of equivalences