4.2 Half adjoint equivalences
In §4.1 (http://planetmath.org/41quasiinverses) we concluded that is equivalent to by discarding a contractible type. Roughly, the type contains three data , , and , of which two ( and ) could together be seen to be contractible when 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.
Thus we have a type , defined to be
Note that in the above definition, the coherence condition relating and only involves . We might consider instead an analogous coherence condition involving :
and a resulting analogous definition .
Fortunately, it turns out each of the conditions implies the other one:
For functions and and homotopies and , the following conditions are logically equivalent:
It suffices to show one direction; the other one is obtained by replacing , , and by , , and respectively. Let . Fix . Using naturality of and applying , we get the following commuting diagram of paths:
Using on the left side of the diagram gives us
Using the commutativity of with (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 as desired. ∎
However, it is important that we do not include both and in the definition of (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.
For any we have .
Suppose that is a quasi-inverse for . We have to provide a quadruple witnessing that is a half adjoint equivalence. To define and , we can just make the obvious choice by setting 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 . Therefore, we can apply Lemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmcor1) to compute
from which we get the desired path . ∎
Combining this with Lemma 4.2.2 (http://planetmath.org/42halfadjointequivalences#Thmprelem1) (or symmetrizing the proof), we also have .
It remains to show that is a mere proposition. For this, we will need to know that the fibers of an equivalence are contractible.
The fiber of a map over a point is
In homotopy theory, this is what would be called the homotopy fiber of . The path lemmas in §2.5 (http://planetmath.org/25thehighergroupoidstructureoftypeformers) yield the following characterization of paths in fibers:
For any , , and , we have
If is a half adjoint equivalence, then for any the fiber is contractible.
Let , and fix . As our center of contraction for we choose . Now take any ; we want to construct a path from to . By Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2), it suffices to give a path such that . We put . Then we have
where the second equality follows by 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 with one of the homotopies.
If has a quasi-inverse, then so do
If is a quasi-inverse of , then and are quasi-inverses of and respectively. ∎
If has a quasi-inverse, then the types and are contractible.
By function extensionality, we have
But this is the fiber of over , 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, is equivalent to the fiber of over and hence contractible. ∎
Next we define the types which put together the other homotopy with the additional coherence datum.
For , a left inverse , and a right inverse , we denote
For any , we have
Using Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2). ∎
If is a half adjoint equivalence, then for any , the type 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 , the type is contractible. But by Theorem 4.2.6 (http://planetmath.org/42halfadjointequivalences#Thmprethm2), is contractible, and any path space of a contractible space is itself contractible. ∎
For any , the type is a mere proposition.
By Lemma 3.11.3 (http://planetmath.org/311contractibility#Thmprelem1) it suffices to assume to be a half adjoint equivalence and show that is contractible. Now by associativity of (http://planetmath.org/node/87641Exercise 2.10), the type 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 has all three desiderata for the type . In the next two sections we consider a couple of other possibilities.
|Title||4.2 Half adjoint equivalences|