Kerodon

Warning 1.2.0.1. Let $f_0, f_1: S \rightarrow T$ be morphisms of simplicial sets. We define a homotopy from $f_0$ to $f_1$ to be a morphism of simplicial sets $h: \Delta ^1 \times S \rightarrow T$ satisfying $h|_{ \{ 0\} \times S} = f_0$ and $h|_{ \{ 1\} \times S} = f_1$ (Definition 3.1.5.2). In the special case where $T = \operatorname{Sing}_{\bullet }(X)$ is the singular simplicial set of a topological space $X$, this recovers the usual definition of homotopy between the associated continuous functions $F_0, F_1: |S| \rightarrow X$ (Example 3.1.5.5). Beware that, if $T$ is a general simplicial set, then the definition of homotopy is not symmetric: the existence of a homotopy from $f_0$ to $f_1$ does not imply the existence of a homotopy from $f_1$ to $f_0$ (for example, take $T = \Delta ^1$ to be the standard simplex, and $f_ i: \{ i\} \hookrightarrow \Delta ^1$ to be the inclusion maps).