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.
In §2.4 (http://planetmath.org/24homotopiesandequivalences) we proved that and . What remains is the following.
For any , the type is a mere proposition.
We may suppose to be bi-invertible and show that is contractible. But since , by Lemma 4.2.9 (http://planetmath.org/42halfadjointequivalences#Thmprelem4) in this case both and 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 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).
For any we have .
We have and . Since both and are mere propositions, the equivalence follows from Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2). ∎
|Title||4.3 Bi-invertible maps|