# Kerodon

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

Proposition 3.1.4.4. Let $X_{}$ and $Y_{}$ be simplicial sets, and suppose we are given a pair of morphisms $f,g: X_{} \rightarrow Y_{}$. Then:

• The morphisms $f$ and $g$ are homotopic if and only if there exists a sequence of morphisms $f = f_0, f_1, \ldots , f_ n = g$ from $X_{}$ to $Y_{}$ having the property that, for each $1 \leq i \leq n$, either there exists a homotopy from $f_{i-1}$ to $f_{i}$ or a homotopy from $f_{i}$ to $f_{i-1}$.

• Suppose that $Y_{}$ is a Kan complex. Then $f$ and $g$ are homotopic if and only if there exists a homotopy from $f$ to $g$.

Proof. The first assertion follows by applying Remark 1.1.6.23 to the simplicial set $\operatorname{Fun}( X_{}, Y_{} )$. If $Y_{}$ is a Kan complex, then $\operatorname{Fun}( X_{}, Y_{} )$ is also a Kan complex (Corollary 3.1.3.4), so the second assertion follows from Proposition 1.1.9.10. $\square$