Definition 7.5.4.1. Let $\operatorname{\mathcal{C}}$ be a category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ be a functor having restriction $\mathscr {F} = \overline{ \mathscr {F} }|_{\operatorname{\mathcal{C}}}$. We will say that $\overline{ \mathscr {F} }$ is a homotopy limit diagram if the composite map
\[ \overline{ \mathscr {F} }( {\bf 0} ) \rightarrow \varprojlim ( \mathscr {F} ) \hookrightarrow \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F} ) \]
is a homotopy equivalence of Kan complexes; here ${\bf 0}$ denotes the initial object of the cone $\operatorname{\mathcal{C}}^{\triangleleft } \simeq \{ {\bf 0} \} \star \operatorname{\mathcal{C}}$, and the morphism on the right is the comparison map of Remark 7.5.2.12).