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 underPlanetmathPlanetmath composition. Furthermore, we have:

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

Suppose f:AB and g:BC. If any two of f, g, and gf are equivalences, so is the third.


If gf and g are equivalences, then (gf)-1g is a quasi-inverse to f. On the one hand, we have (gf)-1gf𝗂𝖽A, while on the other we have

f(gf)-1g g-1gf(gf)-1g

Similarly, if gf and f are equivalences, then f(gf)-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:AB is said to be a retract of a function f:XY if there is a diagram



for which there are

  1. 1.

    a homotopyMathworldPlanetmathPlanetmath R:rs𝗂𝖽A.

  2. 2.

    a homotopy R:rs𝗂𝖽B.

  3. 3.

    a homotopy L:fssg.

  4. 4.

    a homotopy K:grrf.

  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 𝟏. Conversely, just as with contractibility, retractionsMathworldPlanetmathPlanetmath of maps induce retractions of their fibers.

Lemma 4.7.3.

If a function g:AB is a retract of a function f:XY, then fibg(b) is a retract of fibf(s(b)) for every b:B, where s:BY is as in Definition 4.7.2 (http://planetmath.org/47closurepropertiesofequivalences#Thmpredefn1).


Suppose that g:AB is a retract of f:XY. Then for any b:B we have the functions

φb :𝖿𝗂𝖻g(b)𝖿𝗂𝖻f(s(b)), φb(a,p) :(s(a),L(a)\centerdots(p)),
ψb :𝖿𝗂𝖻f(s(b))𝖿𝗂𝖻g(b), ψb(x,q) :(r(x),K(x)\centerdotr(q)\centerdotR(b)).

Then we have ψb(φb(a,p))(r(s(a)),K(s(a))\centerdotr(L(a)\centerdots(p))\centerdotR(b)). We claim ψb is a retraction with sectionPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath φb for all b:B, which is to say that for all (a,p):𝖿𝗂𝖻g(b) we have ψb(φb(a,p))=(a,p). 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 equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to


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


But this transportation computes as g(R(a))-1\centerdotK(s(a))\centerdotr(L(a))\centerdotR(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.


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 contractibleMathworldPlanetmath, 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𝒰 can be viewed as a fibrationMathworldPlanetmath over A with total space (x:A)P(x), the fibration being is the projection 𝗉𝗋1:(x:A)P(x)A. From this point of view, given two type families P,Q:A𝒰, we may refer to a function f:(x:A)(P(x)Q(x)) as a fiberwise map or a fiberwise transformationPlanetmathPlanetmath. Such a map induces a function on total spaces:

Definition 4.7.5.

Given type families P,Q:AU and a map f:(x:A)P(x)Q(x), we define

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


We calculate:

𝖿𝗂𝖻𝗍𝗈𝗍𝖺𝗅(f)((x,v)) w:(x:A)P(x)(𝗉𝗋1w,f(𝗉𝗋1w,𝗉𝗋2w))=(x,v)
(a:A)(u:P(a))(a,f(a,u))=(x,v) (by http://planetmath.org/node/87641Exercise 2.10)
(a:A)(u:P(a))(p:a=x)p*(f(a,u))=v (by Theorem 0.1 (http://planetmath.org/27sigmatypes0.Thmthm1))
u:P(x)f(x,u)=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:(x:A)P(x)Q(x) is a fiberwise equivalence if each f(x):P(x)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 total(f) is an equivalence.


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 𝖿𝗂𝖻𝗍𝗈𝗍𝖺𝗅(f)((x,v)) is contractible if and only if 𝖿𝗂𝖻f(x)(v) is contractible. Thus, 𝖿𝗂𝖻𝗍𝗈𝗍𝖺𝗅(f)(w) is contractible for all w:(x:A)Q(x) if and only if 𝖿𝗂𝖻f(x)(v) is contractible for all x:A and v:Q(x). ∎

Title 4.7 Closure properties of equivalences