Kerodon

Example 7.5.2.2 (Homotopy Limits of Kan Complexes). Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{Kan}$ be a (strictly commutative) diagram of Kan complexes. Then the projection map $U: \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) \rightarrow \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}})$ is a left fibration of simplicial sets (Corollary 5.3.3.19). It follows that every morphism of the $\infty $-category $\operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}})$ is $U$-cocartesian, so the homotopy limit $ \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F})$ of Construction 7.5.2.1 coincides with the homotopy limit $ \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F} )$ of Construction 7.5.1.1.