4.2 Half adjoint equivalences

In Β§4.1 (http://planetmath.org/41quasiinverses) we concluded that π—Šπ—‚π—‡π—β’(f) is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to ∏(x:A)(x=x) by discarding a contractible type. Roughly, the type π—Šπ—‚π—‡π—β’(f) contains three data g, Ξ·, and Ο΅, of which two (g and Ξ·) could together be seen to be contractibleMathworldPlanetmath when f is an equivalence. The problem is that removing these data left one remaining (Ο΅). In order to solve this problem, the idea is to add one additional datum which, together with Ο΅, forms a contractible type.

Definition 4.2.1.

A function f:Aβ†’B is a half adjoint equivalence if there are g:Bβ†’A and homotopiesMathworldPlanetmathPlanetmath Ξ·:g∘f∼idA and Ο΅:f∘g∼idB such that there exists a homotopy


Thus we have a type π—‚π—Œπ—π–Ίπ–Ύβ’(f), defined to be


Note that in the above definition, the coherence condition relating Ξ· and Ο΅ only involves f. We might consider instead an analogous coherence condition involving g:


and a resulting analogous definition π—‚π—Œπ—π–Ίπ–Ύβ€²β’(f).

Fortunately, it turns out each of the conditions implies the other one:

Lemma 4.2.2.

For functions f:Aβ†’B and g:Bβ†’A and homotopies Ξ·:g∘f∼idA and Ο΅:f∘g∼idB, the following conditions are logically equivalent:

  • β€’


  • β€’



It suffices to show one direction; the other one is obtained by replacing A, f, and Ξ· by B, g, and Ο΅ respectively. Let Ο„:∏(x:A)f(Ξ·x)=Ο΅(fx). Fix y:B. Using naturality of Ο΅ and applying g, we get the following commuting diagram of paths:



Using τ⁒(g⁒y) on the left side of the diagram gives us



Using the commutativity of η with g∘f (Definition 2 (http://planetmath.org/24homotopiesandequivalences#Thmdefn2)), we have



However, by naturality of Ξ· we also have



Thus, canceling all but the right-hand homotopy, we have g⁒(ϡ⁒y)=η⁒(g⁒y) as desired. ∎

However, it is important that we do not include both Ο„ and Ο… in the definition of π—‚π—Œπ—π–Ίπ–Ύβ’(f) (whence the name β€œhalf adjoint equivalence”). If we did, then after canceling contractible types we would still have one remaining datum β€” unless we added another higher coherence condition. In general, we expect to get a well-behaved type if we cut off after an odd number of coherences.

Of course, it is obvious that π—‚π—Œπ—π–Ίπ–Ύβ’(f)β†’π—Šπ—‚π—‡π—β’(f): simply forget the coherence datum. The other direction is a version of a standard argument from homotopy theory and category theoryMathworldPlanetmathPlanetmathPlanetmathPlanetmath.

Theorem 4.2.3.

For any f:Aβ†’B we have qinv⁒(f)β†’ishae⁒(f).


Suppose that (g,Ξ·,Ο΅) is a quasi-inverse for f. We have to provide a quadruple (gβ€²,Ξ·β€²,Ο΅β€²,Ο„) witnessing that f is a half adjoint equivalence. To define gβ€² and Ξ·β€², we can just make the obvious choice by setting gβ€²:≑g and Ξ·β€²:≑η. However, in the definition of Ο΅β€² we need start worrying about the construction of Ο„, so we cannot just follow our nose and take Ο΅β€² to be Ο΅. Instead, we take


Now we need to find


Note first that by Corollary 2.4.4 (http://planetmath.org/24homotopiesandequivalences#Thmprelem2), we have Ξ·(g(f(a)))=g(f(Ξ·(a))). Therefore, we can apply Lemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmcor1) to compute

f(Ξ·(g(f(a))))\centerdotΟ΅(f(a)) =f(g(f(Ξ·(a))))\centerdotΟ΅(f(a))

from which we get the desired path τ⁒(a). ∎

Combining this with Lemma 4.2.2 (http://planetmath.org/42halfadjointequivalences#Thmprelem1) (or symmetrizing the proof), we also have π—Šπ—‚π—‡π—β’(f)β†’π—‚π—Œπ—π–Ίπ–Ύβ€²β’(f).

It remains to show that π—‚π—Œπ—π–Ίπ–Ύβ’(f) is a mere proposition. For this, we will need to know that the fibers of an equivalence are contractible.

Definition 4.2.4.

The fiber of a map f:A→B over a point y:B is


In homotopy theory, this is what would be called the homotopy fiber of f. The path lemmas in Β§2.5 (http://planetmath.org/25thehighergroupoidstructureoftypeformers) yield the following characterizationMathworldPlanetmath of paths in fibers:

Lemma 4.2.5.

For any f:Aβ†’B, y:B, and (x,p),(xβ€²,pβ€²):fibf⁒(y), we have

Theorem 4.2.6.

If f:Aβ†’B is a half adjoint equivalence, then for any y:B the fiber fibf⁒(y) is contractible.


Let (g,Ξ·,Ο΅,Ο„):π—‚π—Œπ—π–Ίπ–Ύβ’(f), and fix y:B. As our center of contraction for 𝖿𝗂𝖻f⁒(y) we choose (g⁒y,ϡ⁒y). Now take any (x,p):𝖿𝗂𝖻f⁒(y); we want to construct a path from (g⁒y,ϡ⁒y) to (x,p). By Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2), it suffices to give a path Ξ³:g⁒y=x such that f(Ξ³)\centerdotp=Ο΅y. We put Ξ³:≑g⁒(p)-1\centerdotΞ·x. Then we have

f⁒(γ)⁒\centerdot⁒p =f⁒g⁒(p)-1⁒\centerdot⁒f⁒(η⁒x)⁒\centerdot⁒p

where the second equality follows by τ⁒x and the third equality is naturality of Ο΅. ∎

We now define the types which encapsulate contractible pairs of data. The following types put together the quasi-inverse g with one of the homotopies.

Definition 4.2.7.

Given a function f:A→B, we define the types

𝗅𝗂𝗇𝗏⁒(f) :β‰‘βˆ‘g:Bβ†’A(g∘fβˆΌπ—‚π–½A)
𝗋𝗂𝗇𝗏⁒(f) :β‰‘βˆ‘g:Bβ†’A(f∘gβˆΌπ—‚π–½B)

of left inversesMathworldPlanetmath and right inverses to f, respectively. We call f left invertible if linv⁒(f) is inhabited, and similarly right invertible if rinv⁒(f) is inhabited.

Lemma 4.2.8.

If f:A→B has a quasi-inverse, then so do

(fβˆ˜β€“) :(Cβ†’A)β†’(Cβ†’B)
(β€“βˆ˜f) :(Bβ†’C)β†’(Aβ†’C).

If g is a quasi-inverse of f, then (gβˆ˜β€“) and (β€“βˆ˜g) are quasi-inverses of (fβˆ˜β€“) and (β€“βˆ˜f) respectively. ∎

Lemma 4.2.9.

If f:Aβ†’B has a quasi-inverse, then the types rinv⁒(f) and linv⁒(f) are contractible.


By function extensionality, we have


But this is the fiber of (β€“βˆ˜f) over 𝗂𝖽A, and so by Lemma 4.2.8 (http://planetmath.org/42halfadjointequivalences#Thmprelem3),Theorem 4.2.3 (http://planetmath.org/42halfadjointequivalences#Thmprethm1),Theorem 4.2.6 (http://planetmath.org/42halfadjointequivalences#Thmprethm2), it is contractible. Similarly, 𝗋𝗂𝗇𝗏⁒(f) is equivalent to the fiber of (fβˆ˜β€“) over 𝗂𝖽B and hence contractible. ∎

Next we define the types which put together the other homotopy with the additional coherence datum.

Definition 4.2.10.

For f:Aβ†’B, a left inverse (g,Ξ·):linv⁒(f), and a right inverse (g,Ο΅):rinv⁒(f), we denote

π—…π–Όπ—ˆπ—f⁒(g,Ξ·) :β‰‘βˆ‘(Ο΅:f∘gβˆΌπ—‚π–½B)∏(y:B)g(Ο΅y)=Ξ·(gy),
π—‹π–Όπ—ˆπ—f⁒(g,Ο΅) :β‰‘βˆ‘(Ξ·:g∘fβˆΌπ—‚π–½A)∏(x:A)f(Ξ·x)=Ο΅(fx).
Lemma 4.2.11.

For any f,g,Ο΅,Ξ·, we have

π—…π–Όπ—ˆπ—f⁒(g,Ξ·) β‰ƒβˆy:B(f⁒g⁒y,η⁒(g⁒y))=𝖿𝗂𝖻g⁒(g⁒y)(y,𝗋𝖾𝖿𝗅g⁒y),
π—‹π–Όπ—ˆπ—f⁒(g,Ο΅) β‰ƒβˆx:A(g⁒f⁒x,ϡ⁒(f⁒x))=𝖿𝗂𝖻f⁒(f⁒x)(x,𝗋𝖾𝖿𝗅f⁒x).

Using Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2). ∎

Lemma 4.2.12.

If f is a half adjoint equivalence, then for any (g,ϡ):rinv⁒(f), the type rcohf⁒(g,ϡ) is contractible.


By Lemma 4.2.11 (http://planetmath.org/42halfadjointequivalences#Thmprelem5) and the fact that dependent function types preserve contractible spaces, it suffices to show that for each x:A, the type (g⁒f⁒x,ϡ⁒(f⁒x))=𝖿𝗂𝖻f⁒(f⁒x)(x,𝗋𝖾𝖿𝗅f⁒x) is contractible. But by Theorem 4.2.6 (http://planetmath.org/42halfadjointequivalences#Thmprethm2), 𝖿𝗂𝖻f⁒(f⁒x) is contractible, and any path space of a contractible space is itself contractible. ∎

Theorem 4.2.13.

For any f:Aβ†’B, the type ishae⁒(f) is a mere proposition.


By Lemma 3.11.3 (http://planetmath.org/311contractibility#Thmprelem1) it suffices to assume f to be a half adjoint equivalence and show that π—‚π—Œπ—π–Ίπ–Ύβ’(f) is contractible. Now by associativity of Ξ£ (http://planetmath.org/node/87641Exercise 2.10), the type π—‚π—Œπ—π–Ίπ–Ύβ’(f) is equivalent to


But by Lemma 4.2.9 (http://planetmath.org/42halfadjointequivalences#Thmprelem4),Lemma 4.2.12 (http://planetmath.org/42halfadjointequivalences#Thmprelem6) and the fact that Σ preserves contractibility, the latter type is also contractible. ∎

Thus, we have shown that π—‚π—Œπ—π–Ίπ–Ύβ’(f) has all three desiderata for the type π—‚π—Œπ–Ύπ—Šπ—Žπ—‚π—β’(f). In the next two sectionsPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath we consider a couple of other possibilities.

Title 4.2 Half adjoint equivalences