Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$ $\newcommand\empty{}$

Remark 1.3.6.7. Let $f: X \rightarrow Y$ be a morphism in an $\infty$-category $\operatorname{\mathcal{C}}$. Suppose that $f$ admits a left homotopy inverse $g$ and a right homotopy inverse $h$. Then $g$ and $h$ are homotopic: this follows from the calculation

$[g] = [g] \circ [ \operatorname{id}_ Y ] = [g] \circ ( [f] \circ [h] ) = ( [g] \circ [f] ) \circ [h] = [ \operatorname{id}_ Y ] \circ [h] = [h].$

It follows that both $g$ and $h$ are homotopy inverse to $f$.