Kerodon

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

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

Proof. This is a special case of Corollary 4.4.2.5, since the projection map $U: \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is a left fibration (Corollary 5.3.3.19). $\square$