Kerodon

Proof. We first observe that for any morphism $f: X \rightarrow Y$ in $\operatorname{\mathcal{C}}$, the degenerate $2$-simplex $s^{1}_1(f)$ is a homotopy from $f$ to itself. It follows that homotopy is a reflexive relation on $E$. We will complete the proof by establishing the following:

$(\ast )$

Let $f,g,h: X \rightarrow Y$ be three morphisms from $X$ to $Y$. If $f$ is homotopic to $g$ and $f$ is homotopic to $h$, then $g$ is homotopic to $h$.

Let us first observe that assertion $(\ast )$ implies Proposition 1.4.3.5. Note that in the special case $f = h$, $(\ast )$ asserts that if $f$ is homotopic to $g$, then $g$ is homotopic to $f$ (since $f$ is always homotopic to itself). That is, the relation of homotopy is symmetric. We can therefore replace the hypothesis that $f$ is homotopic to $g$ in assertion $(\ast )$ by the hypothesis that $g$ is homotopic to $f$, so that $(\ast )$ is equivalent to the transitivity of the relation of homotopy.

It remains to prove $(\ast )$. Let $\sigma _2$ and $\sigma _3$ be $2$-simplices of $\operatorname{\mathcal{C}}$ which are homotopies from $f$ to $h$ and $f$ to $g$, respectively, and let $\sigma _0$ be the $2$-simplex given by the constant map $\Delta ^{2} \rightarrow \Delta ^{0} \xrightarrow {Y} \operatorname{\mathcal{C}}$. Then the tuple $( \sigma _0, \bullet , \sigma _2, \sigma _3)$ determines a map of simplicial sets $\tau _0: \Lambda ^3_1 \rightarrow \operatorname{\mathcal{C}}$ (see Proposition 1.2.4.7), depicted informally by the diagram

here the dotted arrows represent the boundary of the “missing” face of the horn $\Lambda ^{3}_1$. Our hypothesis that $\operatorname{\mathcal{C}}$ is an $\infty $-category guarantees that $\tau _0$ can be extended to a $3$-simplex $\tau $ of $\operatorname{\mathcal{C}}$. We can then regard the face $d^{2}_1(\tau )$ as a homotopy from $g$ to $h$. $\square$