Kerodon

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

Variant 7.1.4.14. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a right fibration of $\infty $-categories, let $n$ be an integer such that every fiber of $U$ is $n$-truncated, and let $K$ be an $(n+1)$-connective simplicial set. Then a morphism $\overline{F}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{E}}$ is a limit diagram in $\operatorname{\mathcal{E}}$ if and only if $U \circ \overline{F}$ is a limit diagram in $\operatorname{\mathcal{C}}$. In particular, the functor $U$ preserves $K$-indexed limits.

Proof. Set $F = \overline{F}|_{K}$. Corollary 4.6.4.24 guarantees that $U$ induces a trivial Kan fibration $U_{/F}: \operatorname{\mathcal{E}}_{/F} \rightarrow \operatorname{\mathcal{C}}_{ / (U \circ F)}$. In particular, $\overline{F}$ is final as an object of $\operatorname{\mathcal{E}}_{/F}$ if and only if its image is a final object of $\operatorname{\mathcal{C}}_{ / ( U \circ F)}$. $\square$