Kerodon

Corollary 7.1.6.16. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category, let $K$ be a simplicial set, and let $U: \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) \rightarrow \operatorname{Fun}(K, \operatorname{\mathcal{C}})$ denote the restriction map. Then a morphism of simplicial sets $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ is a limit diagram if and only if it is $U$-final when viewed as an object of the $\infty $-category $\operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}})$.