# 4.3 Bi-invertible maps

Using the language introduced in §4.2 (http://planetmath.org/42halfadjointequivalences), we can restate the definition proposed in §2.4 (http://planetmath.org/24homotopiesandequivalences) as follows.

###### Definition 4.3.1.

We say $f:A\to B$ is bi-invertible if it has both a left inverse  and a right inverse:

 $\mathsf{biinv}(f):\!\!\equiv\mathsf{linv}(f)\times\mathsf{rinv}(f).$

In §2.4 (http://planetmath.org/24homotopiesandequivalences) we proved that $\mathsf{qinv}(f)\to\mathsf{biinv}(f)$ and $\mathsf{biinv}(f)\to\mathsf{qinv}(f)$. What remains is the following.

###### Theorem 4.3.2.

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

###### Proof.

We may suppose $f$ to be bi-invertible and show that $\mathsf{biinv}(f)$ is contractible. But since $\mathsf{biinv}(f)\to\mathsf{qinv}(f)$, by Lemma 4.2.9 (http://planetmath.org/42halfadjointequivalences#Thmprelem4) in this case both $\mathsf{linv}(f)$ and $\mathsf{rinv}(f)$ are contractible, and the product of contractible types is contractible. ∎

Note that this also fits the proposal made at the beginning of §4.2 (http://planetmath.org/42halfadjointequivalences): we combine $g$ and $\eta$ into a contractible type and add an additional datum which combines with $\epsilon$ into a contractible type. The difference is that instead of adding a higher datum (a 2-dimensional path) to combine with $\epsilon$, we add a lower one (a right inverse that is separate from the left inverse).

###### Corollary 4.3.3.

For any $f:A\to B$ we have $\mathsf{biinv}(f)\simeq\mathsf{ishae}(f)$.

###### Proof.

We have $\mathsf{biinv}(f)\to\mathsf{qinv}(f)\to\mathsf{ishae}(f)$ and $\mathsf{ishae}(f)\to\mathsf{qinv}(f)\to\mathsf{biinv}(f)$. Since both $\mathsf{ishae}(f)$ and $\mathsf{biinv}(f)$ are mere propositions, the equivalence follows from Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2). ∎

Title 4.3 Bi-invertible maps
\metatable