# 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:A\to B$ and $g:B\to C$. If any two of $f$, $g$, and $g\circ f$ are equivalences, so is the third.

###### Proof.

If $g\circ f$ and $g$ are equivalences, then $\mathord{{(g\circ f)}^{-1}}\circ g$ is a quasi-inverse to $f$. On the one hand, we have $\mathord{{(g\circ f)}^{-1}}\circ g\circ f\sim\mathsf{id}_{A}$, while on the other we have

 $\displaystyle f\circ\mathord{{(g\circ f)}^{-1}}\circ g$ $\displaystyle\sim\mathord{{g}^{-1}}\circ g\circ f\circ\mathord{{(g\circ f)}^{-% 1}}\circ g$ $\displaystyle\sim\mathord{{g}^{-1}}\circ g$ $\displaystyle\sim\mathsf{id}_{B}.$

Similarly, if $g\circ f$ and $f$ are equivalences, then $f\circ\mathord{{(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:A\to B$ is said to be a retract of a function $f:X\to Y$ if there is a diagram

for which there are

1. 1.

$R:r\circ s\sim\mathsf{id}_{A}$.

2. 2.

a homotopy $R^{\prime}:r^{\prime}\circ s^{\prime}\sim\mathsf{id}_{B}$.

3. 3.

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

4. 4.

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

5. 5.

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

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 $\mathbf{1}$. Conversely, just as with contractibility, retractions of maps induce retractions of their fibers.

###### Lemma 4.7.3.

If a function $g:A\to B$ is a retract of a function $f:X\to Y$, then ${\mathsf{fib}}_{g}(b)$ is a retract of ${\mathsf{fib}}_{f}(s^{\prime}(b))$ for every $b:B$, where $s^{\prime}:B\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

 $\displaystyle\varphi_{b}$ $\displaystyle:{\mathsf{fib}}_{g}(b)\to{\mathsf{fib}}_{f}(s^{\prime}(b)),$ $\displaystyle\varphi_{b}(a,p)$ $\displaystyle:\!\!\equiv{\mathopen{}(s(a),L(a)\mathchoice{\mathbin{\raisebox{2% .15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}% {\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}s^{\prime}(p))% \mathclose{}},$ $\displaystyle\psi_{b}$ $\displaystyle:{\mathsf{fib}}_{f}(s^{\prime}(b))\to{\mathsf{fib}}_{g}(b),$ $\displaystyle\psi_{b}(x,q)$ $\displaystyle:\!\!\equiv{\mathopen{}(r(x),K(x)\mathchoice{\mathbin{\raisebox{2% .15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}% {\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}r^{\prime}(q)% \mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}R^{\prime}(b))\mathclose{}}.$

Then we have $\psi_{b}(\varphi_{b}({a,p}))\equiv{\mathopen{}(r(s(a)),K(s(a))\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}r^{\prime}(% L(a)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}s^{\prime}(p))\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}R^{\prime}(b))\mathclose{}}$. We claim $\psi_{b}$ is a retraction with section $\varphi_{b}$ for all $b:B$, which is to say that for all $(a,p):{\mathsf{fib}}_{g}(b)$ we have $\psi_{b}(\varphi_{b}({a,p}))={\mathopen{}(a,p)\mathclose{}}$. In other words, we want to show

 $\mathchoice{\prod_{(b:B)}\,}{\mathchoice{{\textstyle\prod_{(b:B)}}}{\prod_{(b:% B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b:B)}}}{% \prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}{\mathchoice{{\textstyle\prod_{(b% :B)}}}{\prod_{(b:B)}}{\prod_{(b:B)}}{\prod_{(b:B)}}}\mathchoice{\prod_{(a:A)}% \,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod% _{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_{(a:A)}% }{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)}}{\prod_% {(a:A)}}{\prod_{(a:A)}}}\mathchoice{\prod_{(p:g(a)=b)}\,}{\mathchoice{{% \textstyle\prod_{(p:g(a)=b)}}}{\prod_{(p:g(a)=b)}}{\prod_{(p:g(a)=b)}}{\prod_{% (p:g(a)=b)}}}{\mathchoice{{\textstyle\prod_{(p:g(a)=b)}}}{\prod_{(p:g(a)=b)}}{% \prod_{(p:g(a)=b)}}{\prod_{(p:g(a)=b)}}}{\mathchoice{{\textstyle\prod_{(p:g(a)% =b)}}}{\prod_{(p:g(a)=b)}}{\prod_{(p:g(a)=b)}}{\prod_{(p:g(a)=b)}}}\psi_{b}(% \varphi_{b}({a,p}))={\mathopen{}(a,p)\mathclose{}}.$

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

 $\mathchoice{\prod_{a:A}\,}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod_{(a:A)% }}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}}{\prod% _{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}{\mathchoice{{\textstyle\prod_{(a:A)}}% }{\prod_{(a:A)}}{\prod_{(a:A)}}{\prod_{(a:A)}}}\psi_{g(a)}(\varphi_{g(a)}({a,% \mathsf{refl}_{g(a)}}))={\mathopen{}(a,\mathsf{refl}_{g(a)})\mathclose{}}.$

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)}_{*}\mathopen{}\left({K(s(a))\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}r^{\prime}(L(a))\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}R^{\prime}(% g(a))}\right)\mathclose{}=\mathsf{refl}_{g(a)}.$

But this transportation computes as $\mathord{{g(R(a))}^{-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\,}}}K(s(a))\mathchoice{\mathbin{\raisebox{2.15% pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}r^{\prime}(L(a))\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}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\mathcal{U}$ can be viewed as a fibration over $A$ with total space $\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)$, the fibration being is the projection $\mathsf{pr}_{1}:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}% }{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)\to A$. From this point of view, given two type families $P,Q:A\to\mathcal{U}$, we may refer to a function $f:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\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,Q:A\to\mathcal{U}$ and a map $f:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}P(x)\to Q(x)$, we define

 $\mathsf{total}(f):\!\!\equiv{\lambda}w.\,{\mathopen{}(\mathsf{pr}_{1}w,f(% \mathsf{pr}_{1}w,\mathsf{pr}_{2}w))\mathclose{}}:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}P(x)\to\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}% {\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)% }}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\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:A$ and $v:Q(x)$. Then we have an equivalence

 ${\mathsf{fib}}_{\mathsf{total}(f)}({\mathopen{}(x,v)\mathclose{}})\simeq{% \mathsf{fib}}_{f(x)}(v).$
###### Proof.

We calculate:

 $\displaystyle{\mathsf{fib}}_{\mathsf{total}(f)}({\mathopen{}(x,v)\mathclose{}})$ $\displaystyle\equiv\mathchoice{\sum_{w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x)}\,}{\mathchoice{{\textstyle\sum_{(w:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}P(x))}}}{\sum_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}P(x))}}{\sum_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A% )}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum% _{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x))}}{\sum_{(w:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle\sum_{(w:% \mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{% \sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)% }}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x% :A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x))}}}{\sum_{(w:\mathchoice{\sum_{x:A}\,}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{% (x:A)}}}P(x))}}{\sum_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum% _{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x))}}{% \sum_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_% {(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x))}}}{\mathchoice{{\textstyle% \sum_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_% {(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{% \sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}% }}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x))}}}{\sum_{(w:\mathchoice{% \sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}% }{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:% A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{% (x:A)}}{\sum_{(x:A)}}}P(x))}}{\sum_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x))}}{\sum_{(w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(% x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum% _{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle% \sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x))}}}{\mathopen{}(% \mathsf{pr}_{1}w,f(\mathsf{pr}_{1}w,\mathsf{pr}_{2}w))\mathclose{}}={\mathopen% {}(x,v)\mathclose{}}$ $\displaystyle\simeq\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a% :A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_% {(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle% \sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice{\sum_{(u:% P(a))}\,}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{\sum_{(u:P% (a))}}{\sum_{(u:P(a))}}}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a% ))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{\mathchoice{{\textstyle\sum_{(u:P(a))}% }}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{\mathopen{}(a,f(a,u))% \mathclose{}}={\mathopen{}(x,v)\mathclose{}}{}$ (by http://planetmath.org/node/87641Exercise 2.10) $\displaystyle\simeq\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a% :A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_% {(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle% \sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice{\sum_{(u:% P(a))}\,}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{\sum_{(u:P% (a))}}{\sum_{(u:P(a))}}}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a% ))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{\mathchoice{{\textstyle\sum_{(u:P(a))}% }}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}\mathchoice{\sum_{(p:a=x% )}\,}{\mathchoice{{\textstyle\sum_{(p:a=x)}}}{\sum_{(p:a=x)}}{\sum_{(p:a=x)}}{% \sum_{(p:a=x)}}}{\mathchoice{{\textstyle\sum_{(p:a=x)}}}{\sum_{(p:a=x)}}{\sum_% {(p:a=x)}}{\sum_{(p:a=x)}}}{\mathchoice{{\textstyle\sum_{(p:a=x)}}}{\sum_{(p:a% =x)}}{\sum_{(p:a=x)}}{\sum_{(p:a=x)}}}{p}_{*}\mathopen{}\left({f(a,u)}\right)% \mathclose{}=v{}$ (by Theorem 0.1 (http://planetmath.org/27sigmatypes0.Thmthm1)) $\displaystyle\simeq\mathchoice{\sum_{(a:A)}\,}{\mathchoice{{\textstyle\sum_{(a% :A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle\sum_% {(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}{\mathchoice{{\textstyle% \sum_{(a:A)}}}{\sum_{(a:A)}}{\sum_{(a:A)}}{\sum_{(a:A)}}}\mathchoice{\sum_{(p:% a=x)}\,}{\mathchoice{{\textstyle\sum_{(p:a=x)}}}{\sum_{(p:a=x)}}{\sum_{(p:a=x)% }}{\sum_{(p:a=x)}}}{\mathchoice{{\textstyle\sum_{(p:a=x)}}}{\sum_{(p:a=x)}}{% \sum_{(p:a=x)}}{\sum_{(p:a=x)}}}{\mathchoice{{\textstyle\sum_{(p:a=x)}}}{\sum_% {(p:a=x)}}{\sum_{(p:a=x)}}{\sum_{(p:a=x)}}}\mathchoice{\sum_{(u:P(a))}\,}{% \mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}{% \sum_{(u:P(a))}}}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{\sum_{(u:P(a))}}{% \sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{\mathchoice{{\textstyle\sum_{(u:P(a))}}}{% \sum_{(u:P(a))}}{\sum_{(u:P(a))}}{\sum_{(u:P(a))}}}{p}_{*}\mathopen{}\left({f(% a,u)}\right)\mathclose{}=v$ $\displaystyle\simeq\mathchoice{\sum_{u:P(x)}\,}{\mathchoice{{\textstyle\sum_{(% u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}}{\mathchoice{{% \textstyle\sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}% }{\mathchoice{{\textstyle\sum_{(u:P(x))}}}{\sum_{(u:P(x))}}{\sum_{(u:P(x))}}{% \sum_{(u:P(x))}}}f(x,u)=v{}$ ($*$) $\displaystyle\equiv{\mathsf{fib}}_{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:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\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 $\mathsf{total}(f)$ 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 ${\mathsf{fib}}_{\mathsf{total}(f)}({\mathopen{}(x,v)\mathclose{}})$ is contractible if and only if ${\mathsf{fib}}_{f(x)}(v)$ is contractible. Thus, ${\mathsf{fib}}_{\mathsf{total}(f)}(w)$ is contractible for all $w:\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}% }{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:% A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{% (x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}Q(x)$ if and only if ${\mathsf{fib}}_{f(x)}(v)$ is contractible for all $x:A$ and $v:Q(x)$. ∎

 Title 4.7 Closure properties of equivalences \metatable