Proposition 1.4.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'$.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Let $h''$ be a composition of $f$ and $g'$. Since homotopy is an equivalence relation (Proposition 1.4.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}}$ (Proposition 1.2.4.7), 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^{2}_1(\tau )$ is a homotopy from $h$ to $h''$. $\square$