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!