4.2 Half adjoint equivalences

In §4.1 (http://planetmath.org/41quasiinverses) we concluded that $\mathsf{qinv}(f)$ is equivalent to $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(x=x)$ by discarding a contractible type. Roughly, the type $\mathsf{qinv}(f)$ contains three data $g$ , $\eta$ , and $\epsilon$ , 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 ( $\epsilon$ ). In order to solve this problem, the idea is to add one additional datum which, together with $\epsilon$ , forms a contractible type.

Definition 4.2.1.

A function $f:A\to B$ is a half adjoint equivalence if there are $g:B\to A$ and homotopies $\eta:g\circ f\sim\mathsf{id}_{A}$ and $\epsilon:f\circ g\sim\mathsf{id}_{B}$ such that there exists a homotopy

\tau:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{% (x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{f}\mathopen{}\left({\eta x% }\right)\mathclose{}=\epsilon(fx).

Thus we have a type $\mathsf{ishae}(f)$ , defined to be

\mathchoice{\sum_{(g:B\to A)}\,}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{% \sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{\mathchoice{{% \textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B% \to A)}}}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{% (g:B\to A)}}{\sum_{(g:B\to A)}}}\mathchoice{\sum_{(\eta:g\circ f\sim\mathsf{id% }_{A})}\,}{\mathchoice{{\textstyle\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}{% \sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{id}% _{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}{\mathchoice{{\textstyle% \sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}{\sum_{(\eta:g\circ f\sim\mathsf{id% }_{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}{\sum_{(\eta:g\circ f\sim% \mathsf{id}_{A})}}}{\mathchoice{{\textstyle\sum_{(\eta:g\circ f\sim\mathsf{id}% _{A})}}}{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}{\sum_{(\eta:g\circ f\sim% \mathsf{id}_{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}\mathchoice{\sum% _{(\epsilon:f\circ g\sim\mathsf{id}_{B})}\,}{\mathchoice{{\textstyle\sum_{(% \epsilon:f\circ g\sim\mathsf{id}_{B})}}}{\sum_{(\epsilon:f\circ g\sim\mathsf{% id}_{B})}}{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}{\sum_{(\epsilon:f% \circ g\sim\mathsf{id}_{B})}}}{\mathchoice{{\textstyle\sum_{(\epsilon:f\circ g% \sim\mathsf{id}_{B})}}}{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}{\sum_{(% \epsilon:f\circ g\sim\mathsf{id}_{B})}}{\sum_{(\epsilon:f\circ g\sim\mathsf{id% }_{B})}}}{\mathchoice{{\textstyle\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}% }}{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}{\sum_{(\epsilon:f\circ g\sim% \mathsf{id}_{B})}}{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}}\mathchoice{% \prod_{(x:A)}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{% (x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{% \prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(% x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{f}\mathopen{}\left({\eta x}\right)% \mathclose{}=\epsilon(fx).

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

\upsilon:\mathchoice{\prod_{y:B}\,}{\mathchoice{{\textstyle\prod_{(y:B)}}}{% \prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{\textstyle\prod_{(y% :B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{\textstyle% \prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{g}\mathopen{}% \left({\epsilon y}\right)\mathclose{}=\eta(gy)

and a resulting analogous definition $\mathsf{ishae}^{\prime}(f)$ .

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

Lemma 4.2.2.

For functions $f:A\to B$ and $g:B\to A$ and homotopies $\eta:g\circ f\sim\mathsf{id}_{A}$ and $\epsilon:f\circ g\sim\mathsf{id}_{B}$ , the following conditions are logically equivalent:

•

$\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{f}\mathopen{}\left({\eta x}% \right)\mathclose{}=\epsilon(fx)$
•

$\mathchoice{\prod_{y:B}\,}{\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)% }}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod% _{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{\textstyle\prod_{(y:B)}}% }{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{g}\mathopen{}\left({\epsilon y% }\right)\mathclose{}=\eta(gy)$

Proof.

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

\includegraphics

HoTT_fig_4.2.1.png

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

\includegraphics

HoTT_fig_4.2.2.png

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

\includegraphics

HoTT_fig_4.2.3.png

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

\includegraphics

HoTT_fig_4.2.4.png

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

However, it is important that we do not include both $\tau$ and $\upsilon$ in the definition of $\mathsf{ishae}(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 $\mathsf{ishae}(f)\to\mathsf{qinv}(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:A\to B$ we have $\mathsf{qinv}(f)\to\mathsf{ishae}(f)$ .

Proof.

Suppose that $(g,\eta,\epsilon)$ is a quasi-inverse for $f$ . We have to provide a quadruple $(g^{\prime},\eta^{\prime},\epsilon^{\prime},\tau)$ witnessing that $f$ is a half adjoint equivalence. To define $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 $\epsilon^{\prime}$ we need start worrying about the construction of $\tau$ , so we cannot just follow our nose and take $\epsilon^{\prime}$ to be $\epsilon$ . Instead, we take

\epsilon^{\prime}(b):\!\!\equiv\mathord{{\epsilon(f(g(b)))}^{-1}}\mathchoice{% \mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.1% 5pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}% }}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}({f}% \mathopen{}\left({\eta(g(b))}\right)\mathclose{}\mathchoice{\mathbin{\raisebox% {2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}% }}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\epsilon(b)).

Now we need to find

\tau(a):\mathord{{\epsilon(f(g(f(a))))}^{-1}}\mathchoice{\mathbin{\raisebox{2.% 15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}({f}\mathopen{}\left({\eta(g(f(a% )))}\right)\mathclose{}\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}\epsilon(f(a)))={f}\mathopen{}\left({\eta(% a)}\right)\mathclose{}.

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

	$\displaystyle{f}\mathopen{}\left({\eta(g(f(a)))}\right)\mathclose{}\mathchoice% {\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.% 15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$% }}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\epsilon(f% (a))$	$\displaystyle={f}\mathopen{}\left({{g}\mathopen{}\left({{f}\mathopen{}\left({% \eta(a)}\right)\mathclose{}}\right)\mathclose{}}\right)\mathclose{}\mathchoice% {\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.% 15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$% }}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\epsilon(f% (a))$
		$\displaystyle=\epsilon(f(g(f(a))))\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}{f}\mathopen{}\left({\eta(a)}% \right)\mathclose{}$

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 $\mathsf{qinv}(f)\to\mathsf{ishae}^{\prime}(f)$ .

It remains to show that $\mathsf{ishae}(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\to B$ over a point $y : B$ is

{\mathsf{fib}}_{f}(y):\!\!\equiv\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\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:A\to B$ , $y : B$ , and $(x,p),(x^{\prime},p^{\prime}):{\mathsf{fib}}_{f}(y)$ , we have

\big{(}(x,p)=(x^{\prime},p^{\prime})\big{)}\simeq\Bigl{(}\mathchoice{\sum_{% \gamma:x=x^{\prime}}\,}{\mathchoice{{\textstyle\sum_{(\gamma:x=x^{\prime})}}}{% \sum_{(\gamma:x=x^{\prime})}}{\sum_{(\gamma:x=x^{\prime})}}{\sum_{(\gamma:x=x^% {\prime})}}}{\mathchoice{{\textstyle\sum_{(\gamma:x=x^{\prime})}}}{\sum_{(% \gamma:x=x^{\prime})}}{\sum_{(\gamma:x=x^{\prime})}}{\sum_{(\gamma:x=x^{\prime% })}}}{\mathchoice{{\textstyle\sum_{(\gamma:x=x^{\prime})}}}{\sum_{(\gamma:x=x^% {\prime})}}{\sum_{(\gamma:x=x^{\prime})}}{\sum_{(\gamma:x=x^{\prime})}}}f(% \gamma)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{% \mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1.075pt}{$% \scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$\scriptscriptstyle% \,\centerdot\,$}}}p^{\prime}=p\Bigr{)}

Theorem 4.2.6.

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

Proof.

Let $(g,\eta,\epsilon,\tau):\mathsf{ishae}(f)$ , and fix $y : B$ . As our center of contraction for ${\mathsf{fib}}_{f}(y)$ we choose $(gy,\epsilon y)$ . Now take any $(x,p):{\mathsf{fib}}_{f}(y)$ ; we want to construct a path from $(gy,\epsilon 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}\mathopen{}\left({\gamma}\right)\mathclose{}\mathchoice{\mathbin{\raisebox{% 2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}% }{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{% \raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p=\epsilon y$ . We put $\gamma:\!\!\equiv\mathord{{g(p)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\eta x$ . Then we have

	$\displaystyle f(\gamma)\mathchoice{\mathbin{\raisebox{2.15pt}{$\displaystyle% \centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{\mathbin{\raisebox{1% .075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox{0.43pt}{$% \scriptscriptstyle\,\centerdot\,$}}}p$	$\displaystyle=\mathord{{fg(p)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}f(\eta x)\mathchoice{\mathbin{% \raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p$
		$\displaystyle=\mathord{{fg(p)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{$% \displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$\centerdot$}}}{% \mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{\mathbin{\raisebox% {0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}\epsilon(fx)\mathchoice{\mathbin% {\raisebox{2.15pt}{$\displaystyle\centerdot$}}}{\mathbin{\raisebox{2.15pt}{$% \centerdot$}}}{\mathbin{\raisebox{1.075pt}{$\scriptstyle\,\centerdot\,$}}}{% \mathbin{\raisebox{0.43pt}{$\scriptscriptstyle\,\centerdot\,$}}}p$
		$\displaystyle=\epsilon y$

where the second equality follows by $\tau x$ and the third equality is naturality of $\epsilon$ . ∎

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\to B$ , we define the types

	$\displaystyle\mathsf{linv}(f)$	$\displaystyle:\!\!\equiv\mathchoice{\sum_{g:B\to A}\,}{\mathchoice{{\textstyle% \sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)% }}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B% \to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}(g\circ f\sim\mathsf{id}_{A})$
	$\displaystyle\mathsf{rinv}(f)$	$\displaystyle:\!\!\equiv\mathchoice{\sum_{g:B\to A}\,}{\mathchoice{{\textstyle% \sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)% }}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B% \to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}(f\circ g\sim\mathsf{id}_{B})$

of left inverses and right inverses to $f$ , respectively. We call $f$ left invertible if $\mathsf{linv}(f)$ is inhabited, and similarly right invertible if $\mathsf{rinv}(f)$ is inhabited.

Lemma 4.2.8.

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

	$\displaystyle(f\circ\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$	$\displaystyle:(C\to A)\to(C\to B)$
	$\displaystyle(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ f)$	$\displaystyle:(B\to C)\to(A\to C).$

Proof.

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

Lemma 4.2.9.

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

Proof.

By function extensionality, we have

\mathsf{linv}(f)\simeq\mathchoice{\sum_{g:B\to A}\,}{\mathchoice{{\textstyle% \sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)% }}{\sum_{(g:B\to A)}}}{\mathchoice{{\textstyle\sum_{(g:B\to A)}}}{\sum_{(g:B% \to A)}}{\sum_{(g:B\to A)}}{\sum_{(g:B\to A)}}}(g\circ f=\mathsf{id}_{A}).

But this is the fiber of $(\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt}\circ f)$ over $\mathsf{id}_{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, $\mathsf{rinv}(f)$ is equivalent to the fiber of $(f\circ\mathord{\hskip 1.0pt\text{--}\hskip 1.0pt})$ over $\mathsf{id}_{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\to B$ , a left inverse $(g,\eta):\mathsf{linv}(f)$ , and a right inverse $(g,\epsilon):\mathsf{rinv}(f)$ , we denote

	$\displaystyle\mathsf{lcoh}_{f}(g,\eta)$	$\displaystyle:\!\!\equiv\mathchoice{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B% })}\,}{\mathchoice{{\textstyle\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}}{% \sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}{\sum_{(\epsilon:f\circ g\sim% \mathsf{id}_{B})}}{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}}{\mathchoice% {{\textstyle\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}}{\sum_{(\epsilon:f% \circ g\sim\mathsf{id}_{B})}}{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}{% \sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}}{\mathchoice{{\textstyle\sum_{(% \epsilon:f\circ g\sim\mathsf{id}_{B})}}}{\sum_{(\epsilon:f\circ g\sim\mathsf{% id}_{B})}}{\sum_{(\epsilon:f\circ g\sim\mathsf{id}_{B})}}{\sum_{(\epsilon:f% \circ g\sim\mathsf{id}_{B})}}}\mathchoice{\prod_{(y:B)}\,}{\mathchoice{{% \textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{% \mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y% :B)}}}{\mathchoice{{\textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{% \prod_{(y:B)}}}g(\epsilon y)=\eta(gy),$
	$\displaystyle\mathsf{rcoh}_{f}(g,\epsilon)$	$\displaystyle:\!\!\equiv\mathchoice{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}% \,}{\mathchoice{{\textstyle\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}{\sum_{(% \eta:g\circ f\sim\mathsf{id}_{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}% {\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}{\mathchoice{{\textstyle\sum_{(% \eta:g\circ f\sim\mathsf{id}_{A})}}}{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}% }{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{% id}_{A})}}}{\mathchoice{{\textstyle\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}% {\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{id% }_{A})}}{\sum_{(\eta:g\circ f\sim\mathsf{id}_{A})}}}\mathchoice{\prod_{(x:A)}% \,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod% _{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}% }{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_% {(x:A)}}{\prod_{(x:A)}}}f(\eta x)=\epsilon(fx).$

Lemma 4.2.11.

For any $f,g,\epsilon,\eta$ , we have

	$\displaystyle\mathsf{lcoh}_{f}(g,\eta)$	$\displaystyle\simeq{\mathchoice{\prod_{y:B}\,}{\mathchoice{{\textstyle\prod_{(% y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{\textstyle% \prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}{\mathchoice{{% \textstyle\prod_{(y:B)}}}{\prod_{(y:B)}}{\prod_{(y:B)}}{\prod_{(y:B)}}}(fgy,% \eta(gy))=_{{\mathsf{fib}}_{g}(gy)}(y,\mathsf{refl}_{gy})},$
	$\displaystyle\mathsf{rcoh}_{f}(g,\epsilon)$	$\displaystyle\simeq{\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(% x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(gfx,% \epsilon(fx))=_{{\mathsf{fib}}_{f}(fx)}(x,\mathsf{refl}_{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 $(g,\epsilon):\mathsf{rinv}(f)$ , the type $\mathsf{rcoh}_{f}(g,\epsilon)$ 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,\epsilon(fx))=_{{\mathsf{fib}}_{f}(fx)}(x,\mathsf{refl}_{fx})$ is contractible. But by Theorem 4.2.6 (http://planetmath.org/42halfadjointequivalences#Thmprethm2), ${\mathsf{fib}}_{f}(fx)$ is contractible, and any path space of a contractible space is itself contractible. ∎

Theorem 4.2.13.

For any $f:A\to B$ , the type $\mathsf{ishae}(f)$ 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 $\mathsf{ishae}(f)$ is contractible. Now by associativity of $\Sigma$ (http://planetmath.org/node/87641Exercise 2.10), the type $\mathsf{ishae}(f)$ is equivalent to

\mathchoice{\sum_{u:\mathsf{rinv}(f)}\,}{\mathchoice{{\textstyle\sum_{(u:% \mathsf{rinv}(f))}}}{\sum_{(u:\mathsf{rinv}(f))}}{\sum_{(u:\mathsf{rinv}(f))}}% {\sum_{(u:\mathsf{rinv}(f))}}}{\mathchoice{{\textstyle\sum_{(u:\mathsf{rinv}(f% ))}}}{\sum_{(u:\mathsf{rinv}(f))}}{\sum_{(u:\mathsf{rinv}(f))}}{\sum_{(u:% \mathsf{rinv}(f))}}}{\mathchoice{{\textstyle\sum_{(u:\mathsf{rinv}(f))}}}{\sum% _{(u:\mathsf{rinv}(f))}}{\sum_{(u:\mathsf{rinv}(f))}}{\sum_{(u:\mathsf{rinv}(f% ))}}}\mathsf{rcoh}_{f}(\mathsf{pr}_{1}(u),\mathsf{pr}_{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 $\Sigma$ preserves contractibility, the latter type is also contractible. ∎

Thus, we have shown that $\mathsf{ishae}(f)$ has all three desiderata for the type $\mathsf{isequiv}(f)$ . In the next two sections we consider a couple of other possibilities.

Title	4.2 Half adjoint equivalences
\metatable