Separate homotopy inverses combine into a homotopy equivalence (source code)

= Separate homotopy inverses combine into a homotopy equivalence

If $f:X\to Y$ has maps $g,h:Y\to X$ with $fg\simeq1_Y$ and $hf\simeq1_X$, then $h\simeq hfg\simeq g$, so $g$ is a two-sided homotopy inverse. More generally, if $fg$ and $hf$ are homotopy equivalences, composing $g$ and $h$ with their respective homotopy inverses supplies a right and a left homotopy inverse of $f$, reducing to the first case.