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$ denote the morphism of simplicial sets given on vertices by the formula
\[ T(i,j,k) = \begin{cases} i & \text{ if $k = 0$} \\ j+1 & \text{ if $k=1$} \\ 2 & \text{ if $k=2$.} \end{cases} \]
Then $(\sigma ' \circ T): \Delta ^1 \times \Delta ^1 \times \Delta ^2 \rightarrow \operatorname{\mathcal{C}}$ can be identified with a commutative diagram in the $\infty $-category $\operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}})$, which we depict as
\[ \xymatrix@R =50pt@C=50pt{ \sigma ' \ar [r] \ar [d] & s^{1}_{0}(g') \ar [d] \\ s^{1}_{1}(h') \ar [r] & s_{1}^{1}(g'). } \]
This diagram is a levelwise pullback square, and therefore determines a pullback diagram of morphism spaces
9.46
\begin{equation} \begin{gathered}\label{equation:annoying-proof} \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , \sigma ') \ar [r] \ar [d]^{ \widetilde{\theta } } & \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , s^{1}_{0}(g') ) \ar [d]^{\widetilde{\theta }_0} \\ \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , s^{1}_{1}(h') ) \ar [r]& \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , s_{1}^{1}(g') ) } \end{gathered} \end{equation}
(Proposition 7.4.1.22). Using Corollary 8.3.5.8, we see that $\widetilde{\theta }$ fits into a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , \sigma ') \ar [r] \ar [d]^{ \widetilde{\theta } } \ar [r]^-{\theta } \ar [d] & \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) }( h, h') \ar [d]^{\operatorname{id}} \\ \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , s^{1}_{1}(h') ) \ar [r] & \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) }( h, h'), } \]
where the right vertical map is an identity morphism and the lower horizontal map is a homotopy equivalence by virtue of Corollary 7.3.6.9 (since the degenerate $2$-simplex $s^{1}_{1}(h')$ is right Kan extended from the full subcategory $\operatorname{N}_{\bullet }( \{ 0 < 2 \} ) \subset \Delta ^2$). Consequently, the morphism $\theta $ is a homotopy equivalence if and only if $\widetilde{\theta }$ is a homotopy equivalence. Since the diagram (9.46) is a pullback square, it will suffice to show that $\widetilde{\theta }_0$ is a homotopy equivalence (Corollary 7.6.2.39). We may therefore replace $\sigma '$ by $s^{1}_{0}(g')$, and thereby reduce to the case where $\sigma '$ is left-degenerate (Example 1.1.2.8). Similarly, we may replace $\sigma $ by $s^{1}_{1}(f)$ and thereby reduce to the case where $\sigma $ is right-degenerate. In particular, we may assume that $\sigma $ is left Kan extended from the full subcategory $\Delta ^1 \subset \Delta ^2$. Using Corollary 8.3.5.8 again, we obtain a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , \sigma ') \ar [r] \ar [d]^{ \widetilde{\theta } } \ar [r]^-{\theta } \ar [d] & \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) }( f, f' ) \ar [d]^{\operatorname{id}} \\ \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( \sigma , s^{1}_{1}(h') ) \ar [r] & \operatorname{Hom}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) }( f, h'), } \]
where the horizontal maps are homotopy equivalences (Corollary 7.3.6.9). Since $\sigma '$ is left-degenerate, we have $f' = \operatorname{id}_{Y'}$ and $h' = g'$. We are therefore reduced to proving that the natural map $\operatorname{Hom}_{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) }( f, \operatorname{id}_{Y'} ) \rightarrow \operatorname{Hom}{ \operatorname{Fun}( \Delta ^2, \operatorname{\mathcal{C}}) }( f, g' )$ is a homotopy equivalence, which is a reformulation of our assumption that $f$ is left orthogonal to $g'$ (Lemma 9.6.7.3).
$\square$