Kerodon

Definition 1.4.6.4. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and suppose we are given a pair of morphisms $f: X \rightarrow Y$ and $g: Y \rightarrow X$ in $\operatorname{\mathcal{C}}$. We say that $g$ is a left homotopy inverse of $f$ if the identity morphism $\operatorname{id}_{X}$ is a composition of $f$ and $g$: that is, if we have an equality $[\operatorname{id}_ X] = [g] \circ [f]$ in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$. We say that $g$ is a right homotopy inverse of $f$ if the identity morphism $\operatorname{id}_{Y}$ is a composition of $g$ and $f$: that is, if we have an equality $[ \operatorname{id}_ Y ] = [f] \circ [g]$ in the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$. We will say that $g$ is a homotopy inverse of $f$ if it is both a left and a right homotopy inverse of $f$.