# Kerodon

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

Definition 7.5.4.8 (Homotopy Limit Diagrams of Simplicial Sets). Let $\operatorname{\mathcal{C}}$ be a small category. We say that a functor $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Set_{\Delta }}$ is a homotopy limit diagram if there exists a levelwise weak homotopy equivalence $\alpha : \overline{\mathscr {F}} \rightarrow \overline{\mathscr {G}}$, where $\overline{\mathscr {G}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ is a homotopy limit diagram of Kan complexes (in the sense of Definition 7.5.4.1).