# Kerodon

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

Example 4.5.1.13. Let $f: X \rightarrow Y$ be a morphism of Kan complexes. Then $f$ is a homotopy equivalence if and only if it is an equivalence of $\infty$-categories (see Remark 4.5.1.4). In this case, a morphism $g: Y \rightarrow X$ is a homotopy inverse to $f$ in the sense of Definition 4.5.1.10if and only if it is a homotopy inverse to $f$ in the sense of Definition 3.1.6.1.