# Kerodon

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

Proposition 1.4.3.5. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category containing objects $X,Y \in \operatorname{\mathcal{C}}$, and let $E$ denote the collection of all morphisms from $X$ to $Y$ in $\operatorname{\mathcal{C}}$. Then homotopy is an equivalence relation on $E$.

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

$\xymatrix@C =70pt@R=70pt{ & Y \ar [r]^-{\operatorname{id}_ Y} \ar [drr]^{\operatorname{id}_ Y} & Y \ar@ {-->}[dr]^{\operatorname{id}_ Y}& \\ X \ar [ur]^{f} \ar@ {-->}[urr]^{g} \ar@ {-->}[rrr]^{h} & & & Y; }$

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$