$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Lemma 9.2.8.7. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category containing a lifting problem $\sigma :$
9.20
\begin{equation} \begin{gathered}\label{equation:other-comparison-map-for-Sol} \xymatrix@R =50pt@C=50pt{ A \ar [d]^{f} \ar [r] & X \ar [d]^{g} \\ B \ar [r] \ar@ {-->}[ur]^{s} & Y, } \end{gathered} \end{equation}
which we identify with a morphism from $f$ to $g$ in the $\infty $-category $\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}})$. Then the comparison map $T: {}_{f}\operatorname{Fun}(\Delta ^3, \operatorname{\mathcal{C}})_{g} \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(\Delta ^2,\operatorname{\mathcal{C}})}( \widetilde{f}, \widetilde{g} )$ of Notation 9.2.8.5 restricts to a homotopy equivalence of Kan complexes
\[ T_0: \operatorname{Sol}( \sigma ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(\Delta ^2,\operatorname{\mathcal{C}})}( \widetilde{f}, \widetilde{g} ) \times _{ \operatorname{Hom}_{\operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}) }(f,g) } \{ \sigma \} . \]
Proof.
Let $\alpha : \Delta ^1 \times \Delta ^1 \hookrightarrow \Delta ^3$ be the morphism of simplicial sets given on vertices by the formula $\alpha (i,j) = 2i+j$ (see Definition 9.2.5.1). Then precomposition with $\alpha $ induces an isofibration of $\infty $-categories $U: \operatorname{Fun}( \Delta ^3, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}( \Delta ^1 \times \Delta ^1, \operatorname{\mathcal{C}})$, which restricts to an isofibration $U_0: {}_{f}\operatorname{Fun}(\Delta ^3, \operatorname{\mathcal{C}})_{g} \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) }( f, g )$. Since the source and target of $U_0$ are Kan complexes, it is a Kan fibration (Corollary 4.4.3.10). The desired result now follows by applying Corollary 3.3.7.5 to the diagram of Kan complexes
\[ \xymatrix@R =50pt@C=50pt{ \empty {}_{f}\operatorname{Fun}(\Delta ^3, \operatorname{\mathcal{C}})_{g} \ar [dr]^{U_0} \ar [rr]^{T} & & \operatorname{Hom}_{ \operatorname{Fun}(\Delta ^2,\operatorname{\mathcal{C}})}( \widetilde{f}, \widetilde{g} ) \ar [dl] \\ & \operatorname{Hom}_{ \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}}) }( f, g), & } \]
since $T$ is a homotopy equivalence (Lemma 9.2.8.6).
$\square$