Kerodon

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

Proposition 8.3.6.7. Let $\operatorname{\mathcal{C}}$ be a locally Kan simplicial category. Then the diagram (8.59) is a categorical pullback square.

Proof. Note that the vertical maps in the diagram (8.59) are left fibrations (Propositions 8.1.1.11 and 5.5.3.2). It will therefore suffice to show that, for every pair of objects $X,Y \in \operatorname{\mathcal{C}}$, the induced map of fibers

\begin{eqnarray*} \widetilde{\mathscr {H}}_{X,Y}: \{ X\} \times _{ \operatorname{\mathcal{E}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{E}}) \times _{\operatorname{\mathcal{E}}} \{ Y\} & \rightarrow & \{ \mathscr {H}_{\operatorname{\mathcal{C}}}(X,Y) \} \times _{ \operatorname{\mathcal{S}}} \operatorname{\mathcal{S}}_{\ast } \\ & = & \operatorname{Hom}^{\mathrm{L}}_{\operatorname{\mathcal{S}}}( \Delta ^0, \operatorname{Hom}_{\operatorname{\mathcal{C}}}( X,Y)_{\bullet } ) \end{eqnarray*}

is a homotopy equivalence of Kan complexes (see Corollary 5.1.7.15). Note that the coslice inclusion of Construction 8.1.2.7 induces a monomorphism of simplicial sets $\iota : \operatorname{Hom}_{\operatorname{\mathcal{E}}}^{\mathrm{L}}(X,Y) \hookrightarrow \{ X\} \times _{ \operatorname{\mathcal{E}}^{\operatorname{op}} } \operatorname{Tw}(\operatorname{\mathcal{E}}) \times _{\operatorname{\mathcal{E}}} \{ Y\} $. Unwinding the definitions, we see that the composite map

\[ ( \widetilde{\mathscr {H}}_{X,Y} \circ \iota ): \operatorname{Hom}_{\operatorname{\mathcal{E}}}^{\mathrm{L}}(X,Y) \rightarrow \operatorname{Hom}^{\mathrm{L}}_{\operatorname{\mathcal{S}}}( \Delta ^0, \operatorname{Hom}_{\operatorname{\mathcal{C}}}( X,Y)_{\bullet } ) \]

coincides with isomorphism described in Remark 4.6.8.18. It will therefore suffice to show that $\iota $ is a homotopy equivalence, which is a special case of Corollary 8.1.2.10. $\square$