Kerodon

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

Proposition 9.6.7.4. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category containing $2$-simplices $\sigma $ and $\sigma '$, which we depict as

\[ \xymatrix@R =50pt@C=50pt{ & Y \ar [dr]^{g} & & & Y' \ar [dr]^{g'} & \\ X \ar [ur]^{f} \ar [rr]^{h} & & Z & X' \ar [ur]^{f'} \ar [rr]^{h'} & & Z'. } \]

If $f$ is left orthogonal to $g'$, then the restriction map

\[ \theta : \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , \sigma ' ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) }( h, h' ) \]

is a homotopy equivalence.

Proof. Let $T: \Delta ^1 \times \Delta ^1 \times \Delta ^2 \rightarrow \Delta ^2$ be the morphism of simplicial sets given on vertices by the formula $T(i,j,k) = \begin{cases} i & \end{cases}$ $\square$