# Kerodon

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

Corollary 1.3.3.7. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category, and let $f,g: X \rightarrow Y$ be morphisms of $\operatorname{\mathcal{C}}$ having the same source and target. Then $f$ and $g$ are homotopic (in the sense of Definition 1.3.3.1) if and only if there exists a map of simplicial sets $H: \Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$ satisfying $H|_{ \{ 0\} \times \Delta ^1} = f$, $H|_{ \{ 1\} \times \Delta ^1} = g$, $H|_{ \Delta ^1 \times \{ 0\} } = \operatorname{id}_ X$, and $H|_{ \Delta ^1 \times \{ 1\} } = \operatorname{id}_{Y}$, as indicated in the diagram

$\xymatrix { X \ar [rrrr]^{f} \ar [dddd]^{\operatorname{id}_ X} \ar [ddddrrrr]^{h} & & & & Y \ar [dddd]^{\operatorname{id}_ Y} \\ & & & \sigma & \\ & & & & \\ & \tau & & & \\ X \ar [rrrr]^{g} & & & & Y. }$

Proof. The “only if” direction is clear: if $\sigma$ is a homotopy from $f$ to $g$ (in the sense of Definition 1.3.3.1), then we can extend $\sigma$ to a map $H: \Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$ by taking $\tau$ to be the degenerate simplex $s_0( g )$. Conversely, suppose that there exists a map $\Delta ^1 \times \Delta ^1 \rightarrow \operatorname{\mathcal{C}}$, as indicated in the diagram

$\xymatrix { X \ar [rrrr]^{f} \ar [dddd]^{\operatorname{id}_ X} \ar [ddddrrrr]^{h} & & & & Y \ar [dddd]^{\operatorname{id}_ Y} \\ & & & \sigma & \\ & & & & \\ & \tau & & & \\ X \ar [rrrr]^{g} & & & & Y. }$

Then the $2$-simplex $\sigma$ is a homotopy from $f$ to $h$, and the $2$-simplex $\tau$ guarantees that $g$ is homotopic to $h$ (by virtue of Proposition 1.3.3.6). Since homotopy is an equivalence relation (Proposition 1.3.3.5), it follows that $f$ is homotopic to $g$. $\square$