Kerodon

$\Newextarrow{\xRightarrow}{5,5}{0x21D2}$
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$

Definition 3.2.1.4. Let $(X,x)$ and $(Y,y)$ be pointed simplicial sets, and suppose we are given a pair of pointed maps $f_0, f_1: X \rightarrow Y$. A pointed homotopy from $f_0$ to $f_1$ is a morphism $h: \Delta ^1 \times X_{} \rightarrow Y_{}$ for which $f_0 = h|_{ \{ 0\} \times X_{}}$, $f_1 = h|_{ \{ 1\} \times X_{} }$, and $h|_{ \Delta ^1 \times \{ x\} }$ is the degenerate edge associated to the vertex $y \in Y$.