Kerodon

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

Definition 3.2.1.7. Let $(X,x)$ and $(Y,y)$ be simplicial sets. We say that pointed maps $f_0, f_1: (X,x) \rightarrow (Y,y)$ are pointed homotopic if they are homotopic relative to the simplicial subset $\{ x\} \subseteq X$, in the sense of Definition 3.2.1.3. A pointed homotopy from $f_0$ to $f_1$ is a homotopy $h: \Delta ^1 \times X \rightarrow Y$ which is constant along $\{ x\} $ (Definition 3.2.1.3): that is, which carries $\Delta ^1 \times \{ x\} $ to the degenerate edge $\operatorname{id}_{y}$.