$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 9.1.7.11. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $\sigma :$
9.14
\begin{equation} \begin{gathered}\label{equation:solution-space-as-mapping-space} \xymatrix@R =50pt@C=50pt{ A \ar [d] \ar [r] & X \ar [d] \\ B \ar [r] \ar@ {-->}[ur] & Y } \end{gathered} \end{equation}
be a lifting problem in $\operatorname{\mathcal{C}}$. Then the comparison map
\[ \theta : \operatorname{Hom}_{ \operatorname{\mathcal{C}}_{A/ \, /Y} }( \widetilde{B}, \widetilde{X} ) \rightarrow \operatorname{Sol}( \sigma ) \]
of Construction 9.1.7.10 is a homotopy equivalence of Kan complexes.
Proof.
Corollary 4.6.6.9 supplies a categorical pullback diagram of $\infty $-categories
\[ \xymatrix@R =50pt@C=50pt{ \operatorname{Fun}( \Delta ^1, \operatorname{\mathcal{C}}_{ A / \, / Y} ) \ar [r] \ar [d] & \operatorname{Fun}( \{ A \} \star \Delta ^1 \star \{ Y \} , \operatorname{\mathcal{C}}) \ar [d] \\ \operatorname{Fun}( \operatorname{\partial \Delta }^1, \operatorname{\mathcal{C}}_{ A/ \, /Y} ) \ar [r] & \operatorname{Fun}( \{ A \} \star \operatorname{\partial \Delta }^1 \star \{ Y\} , \operatorname{\mathcal{C}}), } \]
where the vertical maps are isofibrations (Corollary 4.4.5.3). Unwinding the definitions, we see that the comparison map $\theta $ is obtained by taking vertical fibers over the vertex corresponding to the pair $( \widetilde{B}, \widetilde{X} )$. Corollary 4.5.2.31 guarantees that $\theta $ is an equivalence of $\infty $-categories. Since the source and target of $\theta $ are Kan complexes (Remark 9.1.7.3), it is a homotopy equivalence (Example 4.5.1.13).
$\square$