Separate homotopy inverses combine into a homotopy equivalence
ID: separate-homotopy-inverses-combine-into-a-homotopy-equivalence
If has maps with and , then , so is a two-sided homotopy inverse. More generally, if and are homotopy equivalences, composing and with their respective homotopy inverses supplies a right and a left homotopy inverse of , reducing to the first case.
New to topics? Read the docs here!