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:

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

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

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

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 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})}.$

###### 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.