Kerodon

Proof. We will prove $(1)$; the proof of $(2)$ is similar. Let $K$ be a simplicial set and let $p: K \rightarrow \operatorname{\mathcal{C}}_{f/}$ be a diagram, which we will identify with a morphism of simplicial sets $q: A \star K \rightarrow \operatorname{\mathcal{C}}$ satisfying $q|_{A} = f$. Set $g = q|_{K}$, so that $q$ can also be identified with a diagram $f': A \rightarrow \operatorname{\mathcal{C}}_{/g}$. Suppose that $g$ can be extended to a limit diagram $\overline{g}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$. Then the projection map $\operatorname{\mathcal{C}}_{/ \overline{g} } \rightarrow \operatorname{\mathcal{C}}_{/g}$ is a trivial Kan fibration (Proposition 7.1.2.12), so that $f'$ can be lifted to a diagram $f'': A \rightarrow \operatorname{\mathcal{C}}_{ / \overline{g} }$. We can then identify $f''$ with a morphism of simplicial sets $\overline{q}: A \star K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}$ extending $q$, or equivalently with a morphism $\overline{p}: K^{\triangleleft } \rightarrow \operatorname{\mathcal{C}}_{f/}$ extending $p$. We will complete the proof by showing that $\overline{p}$ is a limit diagram. To prove this, it will suffice to show that $\overline{p}$ is final when regarded as an object of the slice $\infty $-category $(\operatorname{\mathcal{C}}_{f/})_{/p} \simeq (\operatorname{\mathcal{C}}_{/g})_{f'/}$. This follows from Proposition 4.6.7.12, since $\overline{g}$ is a final object of $\operatorname{\mathcal{C}}_{/g}$. $\square$