# Kerodon

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

Proposition 7.5.3.12. Let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{QCat}$ be an isofibrant diagram of $\infty$-categories. Then the inclusion map $\iota : \varprojlim ( \mathscr {F} ) \hookrightarrow \underset {\longleftarrow }{\mathrm{holim}}( \mathscr {F} )$ is an equivalence of $\infty$-categories.

Proof. Let $\alpha : \mathscr {F} \hookrightarrow \mathscr {F}^{+}$ be the isofibrant replacement of Construction 7.5.3.3. By virtue of Proposition 7.5.3.7 (and Remark 7.5.3.11), it will suffice to show that the limit $\varprojlim (\alpha ): \varprojlim ( \mathscr {F} ) \hookrightarrow \varprojlim ( \mathscr {F}^{+} )$ is an equivalence of $\infty$-categories. This is a special case of Corollary 4.5.6.16, since $\alpha$ is a levelwise categorical equivalence between isofibrant diagrams (Proposition 7.5.3.4). $\square$