Proposition 7.5.4.5. Let $\operatorname{\mathcal{C}}$ be a small category and let $\overline{\mathscr {F}}: \operatorname{\mathcal{C}}^{\triangleleft } \rightarrow \operatorname{Kan}$ be a diagram of Kan complexes. Then $\overline{\mathscr {F}}$ is a homotopy limit diagram (in the sense of Definition 7.5.4.1) if and only if the induced functor of $\infty $-categories
\[ \operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}}): \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}^{\triangleleft } ) \rightarrow \operatorname{N}_{\bullet }^{\operatorname{hc}}( \operatorname{Kan}) = \operatorname{\mathcal{S}} \]
is a limit diagram (in the sense of Definition 7.1.3.4).
Proof.
Let $\operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft })$ be the weighted nerve of the functor $\overline{\mathscr {F}}$ (Definition 5.3.3.1) and let $U: \operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft }) \rightarrow \operatorname{N}_{\bullet }( \operatorname{\mathcal{C}}^{\triangleleft } )$ be the projection map. Then $U$ is a left fibration, and $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}} )$ is a covariant transport representation for $U$ (Example 5.6.5.6). Set $\mathscr {F} = \overline{\mathscr {F}}|_{\operatorname{\mathcal{C}}}$. Applying Proposition 7.4.1.16, we deduce that $\operatorname{N}_{\bullet }^{\operatorname{hc}}( \overline{\mathscr {F}} )$ is a limit diagram in the $\infty $-category $\operatorname{\mathcal{S}}$ if and only if the restriction map
\[ \rho : \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}^{\triangleleft }) }( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}^{\triangleleft }), \operatorname{N}_{\bullet }^{\overline{\mathscr {F}}}(\operatorname{\mathcal{C}}^{\triangleleft }) ) \rightarrow \simeq \operatorname{Fun}_{ / \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}) }( \operatorname{N}_{\bullet }(\operatorname{\mathcal{C}}), \operatorname{N}_{\bullet }^{\mathscr {F}}(\operatorname{\mathcal{C}}) ) \]
is a homotopy equivalence of Kan complexes. We then have a commutative diagram $\rho $ fits into a commutative diagram
\[ \xymatrix@R =50pt@C=50pt{ \varprojlim ( \overline{ \mathscr {F} } ) \ar [r]^-{\rho '} \ar [d]^{\overline{\iota }} & \varprojlim (\mathscr {F}) \ar [d]^{\iota } \\ \underset {\longleftarrow }{\mathrm{holim}}( \overline{ \mathscr {F} } ) \ar [r]^-{\rho } & \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F}), } \]
where $\iota $ and $\overline{\iota }$ are the comparison maps of Remark 7.5.2.12. Since the category $\operatorname{\mathcal{C}}^{\triangleleft }$ has an initial object, the morphism $\overline{\iota }$ is a homotopy equivalence (Proposition 7.5.2.13). It follows that $\rho $ is a homotopy equivalence if and only if the composition $\rho \circ \overline{\iota } = \iota \circ \rho '$ is a homotopy equivalence. We conclude by observing that the composition $\iota \circ \rho '$ can be identified with the map $\overline{\mathscr {F}}( {\bf 0} ) \rightarrow \underset {\longleftarrow }{\mathrm{holim}}(\mathscr {F})$ appearing in Definition 7.5.4.1.
$\square$