4.2 Half adjoint equivalences

In §4.1 (http://planetmath.org/41quasiinverses) we concluded that $\mathrm{𝗊𝗂𝗇𝗏}(f)$ is equivalent to ${\prod }_{(x:A)}(x=x)$ by discarding a contractible type.Roughly, the type $\mathrm{𝗊𝗂𝗇𝗏}(f)$ contains three data $g$, $\eta$, and $ϵ$, of which two ($g$ and $\eta$) could together be seen to be contractible 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\mathrm{:}A\mathrm{\to }B$ is a half adjoint equivalenceif there are $g\mathrm{:}B\mathrm{\to }A$ and homotopies $\eta \mathrm{:}g\mathrm{\circ }f\mathrm{\sim }{\mathrm{id}}_A$ and $ϵ\mathrm{:}f\mathrm{\circ }g\mathrm{\sim }{\mathrm{id}}_B$ such that there exists a homotopy

$$\tau :\prod _{x:A}f\left(\eta x\right)=ϵ(fx).$$

Thus we have a type $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$, defined to be

$$\sum _{(g:B\to A)}\sum _{(\eta :g\circ f\sim {\mathrm{𝗂𝖽}}_A)}\sum _{(ϵ:f\circ g\sim {\mathrm{𝗂𝖽}}_B)}\prod _{(x:A)}f\left(\eta x\right)=ϵ(fx).$$

Note that in the above definition, the coherence condition relating $\eta$ and $ϵ$ only involves $f$.We might consider instead an analogous coherence condition involving $g$:

$$\upsilon :\prod _{y:B}g\left(ϵy\right)=\eta (gy)$$

and a resulting analogous definition ${\mathrm{𝗂𝗌𝗁𝖺𝖾}}^{\prime }(f)$.

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

Lemma 4.2.2.

For functions $f\mathrm{:}A\mathrm{\to }B$ and $g\mathrm{:}B\mathrm{\to }A$ and homotopies $\eta \mathrm{:}g\mathrm{\circ }f\mathrm{\sim }{\mathrm{id}}_A$ and $ϵ\mathrm{:}f\mathrm{\circ }g\mathrm{\sim }{\mathrm{id}}_B$, the following conditions are logically equivalent:

• ${\prod }_{(x:A)}f\left(\eta x\right)=ϵ(fx)$

• ${\prod }_{(y:B)}g\left(ϵy\right)=\eta (gy)$

Proof.

It suffices to show one direction; the other one is obtained by replacing $A$, $f$, and $\eta$ by $B$, $g$, and $ϵ$ respectively.Let $\tau :{\prod }_{(x:A)}f\left(\eta x\right)=ϵ(fx)$.Fix $y:B$.Using naturality of $ϵ$ and applying $g$, we get the following commuting diagram of paths:

HoTT_fig_4.2.1.png

Using $\tau (gy)$ on the left side of the diagram gives us

HoTT_fig_4.2.2.png

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

HoTT_fig_4.2.3.png

However, by naturality of $\eta$ we also have

HoTT_fig_4.2.4.png

Thus, canceling all but the right-hand homotopy, we have $g(ϵy)=\eta (gy)$ as desired.∎

However, it is important that we do not include both $\tau$ and $\upsilon$ in the definition of $\mathrm{𝗂𝗌𝗁𝖺𝖾}(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 $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)\to \mathrm{𝗊𝗂𝗇𝗏}(f)$: simply forget the coherence datum.The other direction is a version of a standard argument from homotopy theory and category theory.

Theorem 4.2.3.

For any $f\mathrm{:}A\mathrm{\to }B$ we have $\mathrm{qinv}\mathit{}\mathrm{(}f\mathrm{)}\mathrm{\to }\mathrm{ishae}\mathit{}\mathrm{(}f\mathrm{)}$.

Proof.

Suppose that $(g,\eta ,ϵ)$ is a quasi-inverse for $f$. We have to providea quadruple $(g^{\prime },{\eta }^{\prime },{ϵ}^{\prime },\tau )$ witnessing that $f$ is a half adjoint equivalence. Todefine $g^{\prime }$ and ${\eta }^{\prime }$, we can just make the obvious choice by setting $g^{\prime }:\equiv g$ and ${\eta }^{\prime }:\equiv \eta$. However, in the definition of ${ϵ}^{\prime }$ weneed start worrying about the construction of $\tau$, so we cannot just follow our noseand take ${ϵ}^{\prime }$ to be $ϵ$. Instead, we take

$${ϵ}^{\prime }(b):\equiv ϵ{(f(g(b)))}^{-1}(f\left(\eta (g(b))\right)ϵ(b)).$$

Now we need to find

$$\tau (a):ϵ{(f(g(f(a))))}^{-1}(f\left(\eta (g(f(a)))\right)ϵ(f(a)))=f\left(\eta (a)\right).$$

Note first that by Corollary 2.4.4 (http://planetmath.org/24homotopiesandequivalences#Thmprelem2), we have$\eta (g(f(a)))=g\left(f\left(\eta (a)\right)\right)$. Therefore, we can applyLemma 2.4.3 (http://planetmath.org/24homotopiesandequivalences#Thmcor1) to compute

$f\left(\eta (g(f(a)))\right)ϵ(f(a))$$=f\left(g\left(f\left(\eta (a)\right)\right)\right)ϵ(f(a))$

$=ϵ(f(g(f(a))))f\left(\eta (a)\right)$

from which we get the desired path $\tau (a)$.∎

Combining this with Lemma 4.2.2 (http://planetmath.org/42halfadjointequivalences#Thmprelem1) (or symmetrizing the proof), we also have $\mathrm{𝗊𝗂𝗇𝗏}(f)\to {\mathrm{𝗂𝗌𝗁𝖺𝖾}}^{\prime }(f)$.

It remains to show that $\mathrm{𝗂𝗌𝗁𝖺𝖾}(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 fiberof a map $f\mathrm{:}A\mathrm{\to }B$ over a point $y\mathrm{:}B$ is

$${\mathrm{𝖿𝗂𝖻}}_f(y):\equiv \sum _{x:A}(f(x)=y).$$

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 characterization of paths in fibers:

Lemma 4.2.5.

For any $f\mathrm{:}A\mathrm{\to }B$, $y\mathrm{:}B$, and $\mathrm{(}x\mathrm{,}p\mathrm{)}\mathrm{,}\mathrm{(}{x}^{\mathrm{\prime }}\mathrm{,}{p}^{\mathrm{\prime }}\mathrm{)}\mathrm{:}{\mathrm{fib}}_f\mathit{}\mathrm{(}y\mathrm{)}$, we have

$$((x,p)=(x^{\prime },p^{\prime }))\simeq (\sum _{\gamma :x=x^{\prime }}f(\gamma )p^{\prime }=p)$$

Theorem 4.2.6.

If $f\mathrm{:}A\mathrm{\to }B$ is a half adjoint equivalence, then for any $y\mathrm{:}B$ the fiber ${\mathrm{fib}}_f\mathit{}\mathrm{(}y\mathrm{)}$ is contractible.

Proof.

Let $(g,\eta ,ϵ,\tau ):\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$, and fix $y:B$.As our center of contraction for ${\mathrm{𝖿𝗂𝖻}}_f(y)$ we choose $(gy,ϵy)$.Now take any $(x,p):{\mathrm{𝖿𝗂𝖻}}_f(y)$; we want to construct a path from $(gy,ϵy)$ to $(x,p)$.By Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2), it suffices to give a path $\gamma :gy=x$ such that $f\left(\gamma \right)p=ϵy$.We put $\gamma :\equiv g{(p)}^{-1}\eta x$.Then we have

$f(\gamma )p$$=fg{(p)}^{-1}f(\eta x)p$

$=fg{(p)}^{-1}ϵ(fx)p$

$=ϵy$

where the second equality follows by $\tau 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\mathrm{:}A\mathrm{\to }B$, we define the types

$\mathrm{𝗅𝗂𝗇𝗏}(f)$$:\equiv {\displaystyle \sum _{g:B\to A}}(g\circ f\sim {\mathrm{𝗂𝖽}}_A)$

$\mathrm{𝗋𝗂𝗇𝗏}(f)$$:\equiv {\displaystyle \sum _{g:B\to A}}(f\circ g\sim {\mathrm{𝗂𝖽}}_B)$

of left inversesand right inversesto $f$, respectively.We call $f$ left invertibleif $\mathrm{linv}\mathit{}\mathrm{(}f\mathrm{)}$ is inhabited, and similarly right invertibleif $\mathrm{rinv}\mathit{}\mathrm{(}f\mathrm{)}$ is inhabited.

Lemma 4.2.8.

If $f\mathrm{:}A\mathrm{\to }B$ has a quasi-inverse, then so do

$(f\circ \mathit{\text{–}})$$:(C\to A)\to (C\to B)$

$(\mathit{\text{–}}\circ f)$$:(B\to C)\to (A\to C).$

Proof.

If $g$ is a quasi-inverse of $f$, then $(g\circ \text{–})$ and $(\text{–}\circ g)$ are quasi-inverses of $(f\circ \text{–})$ and $(\text{–}\circ f)$ respectively.∎

Lemma 4.2.9.

If $f\mathrm{:}A\mathrm{\to }B$ has a quasi-inverse, then the types $\mathrm{rinv}\mathit{}\mathrm{(}f\mathrm{)}$ and $\mathrm{linv}\mathit{}\mathrm{(}f\mathrm{)}$ are contractible.

Proof.

By function extensionality, we have

$$\mathrm{𝗅𝗂𝗇𝗏}(f)\simeq \sum _{g:B\to A}(g\circ f={\mathrm{𝗂𝖽}}_A).$$

But this is the fiber of $(\text{–}\circ f)$ over ${\mathrm{𝗂𝖽}}_A$, and soby 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, $\mathrm{𝗋𝗂𝗇𝗏}(f)$ is equivalent to the fiber of $(f\circ \text{–})$ over ${\mathrm{𝗂𝖽}}_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\mathrm{:}A\mathrm{\to }B$, a left inverse $\mathrm{(}g\mathrm{,}\eta \mathrm{)}\mathrm{:}\mathrm{linv}\mathit{}\mathrm{(}f\mathrm{)}$, and a right inverse $\mathrm{(}g\mathrm{,}ϵ\mathrm{)}\mathrm{:}\mathrm{rinv}\mathit{}\mathrm{(}f\mathrm{)}$, we denote

${\mathrm{𝗅𝖼𝗈𝗁}}_f(g,\eta )$$:\equiv {\displaystyle \sum _{(ϵ:f\circ g\sim {\mathrm{𝗂𝖽}}_B)}}{\displaystyle \prod _{(y:B)}}g(ϵy)=\eta (gy),$

${\mathrm{𝗋𝖼𝗈𝗁}}_f(g,ϵ)$$:\equiv {\displaystyle \sum _{(\eta :g\circ f\sim {\mathrm{𝗂𝖽}}_A)}}{\displaystyle \prod _{(x:A)}}f(\eta x)=ϵ(fx).$

Lemma 4.2.11.

For any $f\mathrm{,}g\mathrm{,}ϵ\mathrm{,}\eta$, we have

${\mathrm{𝗅𝖼𝗈𝗁}}_f(g,\eta )$$\simeq {\displaystyle \prod _{y:B}}(fgy,\eta (gy)){=}_{{\mathrm{𝖿𝗂𝖻}}_g(gy)}(y,{\mathrm{𝗋𝖾𝖿𝗅}}_{gy}),$

${\mathrm{𝗋𝖼𝗈𝗁}}_f(g,ϵ)$$\simeq {\displaystyle \prod _{x:A}}(gfx,ϵ(fx)){=}_{{\mathrm{𝖿𝗂𝖻}}_f(fx)}(x,{\mathrm{𝗋𝖾𝖿𝗅}}_{fx}).$

Proof.

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

Lemma 4.2.12.

If $f$ is a half adjoint equivalence, then for any $\mathrm{(}g\mathrm{,}ϵ\mathrm{)}\mathrm{:}\mathrm{rinv}\mathit{}\mathrm{(}f\mathrm{)}$, the type ${\mathrm{rcoh}}_f\mathit{}\mathrm{(}g\mathrm{,}ϵ\mathrm{)}$ is contractible.

Proof.

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 $(gfx,ϵ(fx)){=}_{{\mathrm{𝖿𝗂𝖻}}_f(fx)}(x,{\mathrm{𝗋𝖾𝖿𝗅}}_{fx})$ is contractible.But by Theorem 4.2.6 (http://planetmath.org/42halfadjointequivalences#Thmprethm2), ${\mathrm{𝖿𝗂𝖻}}_f(fx)$ is contractible, and any path space of a contractible space is itself contractible.∎

Theorem 4.2.13.

For any $f\mathrm{:}A\mathrm{\to }B$, the type $\mathrm{ishae}\mathit{}\mathrm{(}f\mathrm{)}$ is a mere proposition.

Proof.

By Lemma 3.11.3 (http://planetmath.org/311contractibility#Thmprelem1) it suffices to assume $f$ to be a half adjoint equivalence and show that $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$ is contractible.Now by associativity of $\mathrm{\Sigma }$ (http://planetmath.org/node/87641Exercise 2.10), the type $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$ is equivalent to

$$\sum _{u:\mathrm{𝗋𝗂𝗇𝗏}(f)}{\mathrm{𝗋𝖼𝗈𝗁}}_f({\mathrm{𝗉𝗋}}_1(u),{\mathrm{𝗉𝗋}}_2(u)).$$

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

Thus, we have shown that $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$ has all three desiderata for the type $\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$.In the next two sections we consider a couple of other possibilities.