# Kerodon

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

Proposition 1.3.4.7. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category. Suppose we are given a pair of homotopic morphisms $f,f': X \rightarrow Y$ in $\operatorname{\mathcal{C}}$ and a pair of homotopic morphisms $g,g': Y \rightarrow Z$ in $\operatorname{\mathcal{C}}$. Let $h$ be a composition of $f$ and $g$, and let $h'$ be a composition of $f'$ and $g'$. Then $h$ is homotopic to $h'$.

Proof. Let $h''$ be a composition of $f$ and $g'$. Since homotopy is an equivalence relation (Proposition 1.3.3.5), it will suffice to show that both $h$ and $h'$ are homotopic to $h''$. We will show that $h$ is homotopic to $h''$; the proof that $h'$ is homotopic to $h''$ is similar. Let $\sigma _3$ be a $2$-simplex of $\operatorname{\mathcal{C}}$ which witnesses $h$ as a composition of $f$ and $g$, let $\sigma _2$ be a $2$-simplex of $\operatorname{\mathcal{C}}$ which witnesses $h''$ as a composition of $f$ and $g'$, and let $\sigma _0$ be a $2$-simplex of $\operatorname{\mathcal{C}}$ which is a homotopy from $g$ to $g'$. 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}}$ (Exercise 1.1.2.14), which we depict informally as a diagram

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

where the dotted arrows indicate the boundary of the “missing” face of the horn $\Lambda ^{3}_{1}$. Using our assumption that $\operatorname{\mathcal{C}}$ is an $\infty$-category, we can extend $\tau _0$ to a $3$-simplex $\tau$ of $\operatorname{\mathcal{C}}$. Then the face $d_1(\tau )$ is a homotopy from $h$ to $h''$. $\square$