Kerodon

Remark 1.4.6.6. Let $f: X \rightarrow Y$ and $g: Y \rightarrow X$ be morphisms in an $\infty $-category $\operatorname{\mathcal{C}}$. Then $g$ is left homotopy inverse to $f$ if and only if $f$ is right homotopy inverse to $g$. Both of these conditions are equivalent to the existence of a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$ satisfying $d^{2}_0(\sigma ) = g$, $d^{2}_1(\sigma ) = \operatorname{id}_{X}$, and $d^{2}_2(\sigma ) = f$, as depicted in the diagram