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→B is bi-invertible if it has both a left inverseMathworldPlanetmath and a right inverse:


In Β§2.4 (http://planetmath.org/24homotopiesandequivalences) we proved that π—Šπ—‚π—‡π—β’(f)→𝖻𝗂𝗂𝗇𝗏⁒(f) and 𝖻𝗂𝗂𝗇𝗏⁒(f)β†’π—Šπ—‚π—‡π—β’(f). What remains is the following.

Theorem 4.3.2.

For any f:Aβ†’B, the type biinv⁒(f) is a mere proposition.


We may suppose f to be bi-invertible and show that 𝖻𝗂𝗂𝗇𝗏⁒(f) is contractible. But since 𝖻𝗂𝗂𝗇𝗏⁒(f)β†’π—Šπ—‚π—‡π—β’(f), by Lemma 4.2.9 (http://planetmath.org/42halfadjointequivalences#Thmprelem4) in this case both 𝗅𝗂𝗇𝗏⁒(f) and 𝗋𝗂𝗇𝗏⁒(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 Ξ· 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:Aβ†’B we have biinv⁒(f)≃ishae⁒(f).


We have 𝖻𝗂𝗂𝗇𝗏⁒(f)β†’π—Šπ—‚π—‡π—β’(f)β†’π—‚π—Œπ—π–Ίπ–Ύβ’(f) and π—‚π—Œπ—π–Ίπ–Ύβ’(f)β†’π—Šπ—‚π—‡π—β’(f)→𝖻𝗂𝗂𝗇𝗏⁒(f). Since both π—‚π—Œπ—π–Ίπ–Ύβ’(f) and 𝖻𝗂𝗂𝗇𝗏⁒(f) are mere propositions, the equivalence follows from Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2). ∎

Title 4.3 Bi-invertible maps