We have already seen in Lemma 2.4.12 (http://planetmath.org/http://planetmath.org/24homotopiesandequivalences#Thmprelem3) that equivalences are closed undercomposition.
Furthermore, we have:
Theorem 4.7.1 (The 2-out-of-3 property).
Suppose and .
If any two of , , and are equivalences, so is the third.
Proof.
If and are equivalences, then is a quasi-inverse to .
On the one hand, we have , while on the other we have
Similarly, if and are equivalences, then is a quasi-inverse to .
∎
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 is said to be a retract
of a function if there is a diagram
for every , a path witnessing the commutativity of the square
\includegraphics
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 and are .
Conversely, just as with contractibility, retractions of maps induce retractions of their fibers.
Lemma 4.7.3.
If a function is a retract of a function , then is a retract of
for every , where is as in Definition 4.7.2 (http://planetmath.org/47closurepropertiesofequivalences#Thmpredefn1).
Proof.
Suppose that is a retract of . Then for any we have the functions
Then we have .
We claim is a retraction with section for all , which is to say that for all we have .
In other words, we want to show
By reordering the first two s and applying a version of Lemma 3.11.9 (http://planetmath.org/311contractibility#Thmprelem6), this is equivalent to
For any , 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 , so we need only show
But this transportation computes as , so the required path is given by .
∎
Theorem 4.7.4.
If is a retract of an equivalence , then is also an equivalence.
Proof.
By Lemma 4.7.3 (http://planetmath.org/47closurepropertiesofequivalences#Thmprelem1), every fiber of is a retract of a fiber of .
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 can be viewed as a fibration over with total space , the fibration being is the projection .
From this point of view, given two type families , we may refer to a function as a fiberwise map or a fiberwise transformation.
Such a map induces a function on total spaces:
Definition 4.7.5.
Given type families and a map , we define
Theorem 4.7.6.
Suppose that is a fiberwise transformation between families and
over a type and let and . Then we have an equivalence
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 is a fiberwise equivalence
if each is an equivalence.
Theorem 4.7.7.
Suppose that is a fiberwise transformation between families
and over a type .
Then is a fiberwise equivalence if and only if is an equivalence.
Proof.
Let , , and be as in the statement of the theorem.
By Theorem 4.7.6 (http://planetmath.org/47closurepropertiesofequivalences#Thmprethm3) it follows for all
and that
is contractible if and only if
is contractible.
Thus, is contractible for all if and only if is contractible for all and .
∎