Kerodon

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

Remark 7.1.2.6. Let $\overline{u}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ be as in Definition 7.1.2.4. Then $\overline{u}$ is a limit diagram if and only if the composite map

\[ \Delta ^1 \times K \simeq K \star _{K} K \rightarrow \Delta ^0 \star _{ \Delta ^0} K = K^{\triangleleft } \xrightarrow {\overline{u}} \operatorname{\mathcal{C}} \]

corresponds to a natural transformation $\alpha : \underline{Y} \rightarrow u$ which exhibits $Y$ as a limit of $u$, in the sense of Definition 7.1.1.1. This follows from the characterization of Proposition 7.1.2.1, together with the observation that the slice diagonal $\operatorname{\mathcal{C}}_{/u} \hookrightarrow \operatorname{\mathcal{C}}\operatorname{\vec{\times }}_{ \operatorname{Fun}(K, \operatorname{\mathcal{C}})} \{ u\} $ of Construction 4.6.4.13 is an equivalence of $\infty $-categories (Theorem 4.6.4.17).