Kerodon

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

Proposition 9.2.7.11. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category and let $\sigma :$

9.16
\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.2.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.2.7.3), it is a homotopy equivalence (Example 4.5.1.13). $\square$