Kerodon

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

Proposition 1.4.3.6. 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 if and only if they are homotopic when regarded as morphisms of the opposite $\infty $-category $\operatorname{\mathcal{C}}^{\operatorname{op}}$. In other words, the following conditions are equivalent:

$(1)$

There exists a $2$-simplex $\sigma $ of $\operatorname{\mathcal{C}}$ satisfying $d^{2}_0( \sigma ) = \operatorname{id}_{Y}$, $d^{2}_1(\sigma ) = g$, and $d^{2}_2(\sigma ) = f$, as depicted in the diagram

\[ \xymatrix@R =50pt@C=50pt{ & Y \ar [dr]^{\operatorname{id}_ Y} & \\ X \ar [ur]^{f} \ar [rr]^{g} & & Y. } \]
$(2)$

There exists a $2$-simplex $\tau $ of $\operatorname{\mathcal{C}}$ satisfying $d^{2}_0( \tau ) = f$, $d^{2}_1(\tau ) = g$, and $d^{2}_2(\tau ) = \operatorname{id}_ X$, as depicted in the diagram

\[ \xymatrix@R =50pt@C=50pt{ & X \ar [dr]^{f} & \\ X \ar [ur]^{\operatorname{id}_ X} \ar [rr]^{g} & & Y. } \]

Proof. We will show that $(1)$ implies $(2)$; the proof of the reverse implication is similar. Assume that $f$ is homotopic to $g$. Since the relation of homotopy is symmetric (Proposition 1.4.3.5), it follows that $g$ is also homotopic to $f$. Let $\sigma $ be a homotopy from $g$ to $f$. Then we can regard the tuple of $2$-simplices $( \sigma , s^{1}_1(g), \bullet , s^{1}_0(g) )$ as a map of simplicial sets $\rho _0: \Lambda ^{3}_{2} \rightarrow \operatorname{\mathcal{C}}$ (see Proposition 1.2.4.7), depicted informally in the diagram

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

where the dotted arrows indicate the boundary of the “missing” face of the horn $\Lambda ^{3}_{2}$. Using our assumption that $\operatorname{\mathcal{C}}$ is an $\infty $-category, we can extend $\rho _0$ to a $3$-simplex $\rho $ of $\operatorname{\mathcal{C}}$. Then the face $\tau = d^{3}_2(\rho )$ has the properties required by $(2)$. $\square$