Corollary 7.1.6.14. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a cocartesian fibration of $\infty $-categories. Then a morphism of simplicial sets $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ is a $U$-limit diagram if and only if it is final when viewed as an object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( K^{\triangleleft }, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( K, \operatorname{\mathcal{C}}) } \{ \overline{f}|_{K} \} $.
$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proof. Since $U$ is a cocartesian fibration, Corollary 5.3.7.4 guarantees that the induced map
\[ U': \operatorname{Fun}( K^{\triangleleft }, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K,\operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}(K, \operatorname{\mathcal{D}}) } \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{D}}) \]
is also a cocartesian fibration. It follows that $\overline{f}$ is a final object of the $\infty $-category $\operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( K^{\triangleleft }, \operatorname{\mathcal{C}}) \times _{ \operatorname{Fun}_{ / \operatorname{\mathcal{D}}}( K, \operatorname{\mathcal{C}}) } \{ \overline{f}|_{K} \} $ if and only if is $U'$-final when viewed as an object of $\operatorname{Fun}( K^{\triangleleft }, \operatorname{\mathcal{C}})$ (Corollary 7.1.5.21). The desired result now follows from Proposition 7.1.6.13. $\square$