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\mathrm{:}A\mathrm{\to }B$ is bi-invertibleif it has both a left inverse and a right inverse:

$$\mathrm{𝖻𝗂𝗂𝗇𝗏}(f):\equiv \mathrm{𝗅𝗂𝗇𝗏}(f)\times \mathrm{𝗋𝗂𝗇𝗏}(f).$$

In §2.4 (http://planetmath.org/24homotopiesandequivalences) we proved that $\mathrm{𝗊𝗂𝗇𝗏}(f)\to \mathrm{𝖻𝗂𝗂𝗇𝗏}(f)$ and $\mathrm{𝖻𝗂𝗂𝗇𝗏}(f)\to \mathrm{𝗊𝗂𝗇𝗏}(f)$.What remains is the following.

Theorem 4.3.2.

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

Proof.

We may suppose $f$ to be bi-invertible and show that $\mathrm{𝖻𝗂𝗂𝗇𝗏}(f)$ is contractible.But since $\mathrm{𝖻𝗂𝗂𝗇𝗏}(f)\to \mathrm{𝗊𝗂𝗇𝗏}(f)$, by Lemma 4.2.9 (http://planetmath.org/42halfadjointequivalences#Thmprelem4) in this case both $\mathrm{𝗅𝗂𝗇𝗏}(f)$ and $\mathrm{𝗋𝗂𝗇𝗏}(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 $ϵ$ into a contractible type.The difference is that instead of adding a higher datum (a 2-dimensional path) to combine with $ϵ$, we add a lower one (a right inverse that is separate from the left inverse).

Corollary 4.3.3.

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

Proof.

We have $\mathrm{𝖻𝗂𝗂𝗇𝗏}(f)\to \mathrm{𝗊𝗂𝗇𝗏}(f)\to \mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$ and $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)\to \mathrm{𝗊𝗂𝗇𝗏}(f)\to \mathrm{𝖻𝗂𝗂𝗇𝗏}(f)$.Since both $\mathrm{𝗂𝗌𝗁𝖺𝖾}(f)$ and $\mathrm{𝖻𝗂𝗂𝗇𝗏}(f)$ are mere propositions, the equivalence follows from Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2).∎