Kerodon

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

Corollary 7.1.6.14. Let $\operatorname{\mathcal{C}}$ be an $\infty $-category. Then a morphism $\overline{f}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ is a limit diagram if and only if, for every object $C \in \operatorname{\mathcal{C}}$, the restriction map

\[ \operatorname{Hom}_{ \operatorname{Fun}(K^{\triangleleft }, \operatorname{\mathcal{C}}) }( \underline{C}, \overline{f} ) \rightarrow \operatorname{Hom}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}}) }( \underline{C}|_{K}, \overline{f}|_{K} ) \]

is a homotopy equivalence of Kan complexes.