Kerodon

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

Proposition 7.5.1.5. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Kan}$ be a diagram of Kan complexes. Then the Kan complex $ \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F})$ is a limit of the diagram

\[ \operatorname{N}_{\bullet }^{\operatorname{hc}}( \mathscr {F}): \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Kan}) = \operatorname{\mathcal{S}} \]

in the $\infty $-category $\operatorname{\mathcal{S}}$.

Proof. This is a special case of Proposition 7.4.1.6, since the functor $\operatorname{N}_{\bullet }^{\operatorname{hc}}(\mathscr {F} )$ is a covariant transport representation for the projection map $U: \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ (Example 5.6.5.6). $\square$