Kerodon

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

Corollary 7.3.3.23. Let $U: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be an inner fibration of $\infty $-categories, let $\operatorname{\mathcal{D}}_{E} = \{ E\} \times _{\operatorname{\mathcal{E}}} \operatorname{\mathcal{D}}$ be the fiber of $U$ over an object $E \in \operatorname{\mathcal{E}}$, let $F: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}_{E}$ be a functor of $\infty $-categories, and $\operatorname{\mathcal{C}}^{0} \subseteq \operatorname{\mathcal{C}}$ be a full subcategory. If $F$ is $U$-left Kan extended from $\operatorname{\mathcal{C}}^{0}$ (when regarded as a functor from $\operatorname{\mathcal{C}}$ to $\operatorname{\mathcal{D}}$), then it is left Kan extended from $\operatorname{\mathcal{C}}^{0}$ (when regarded as a functor from $\operatorname{\mathcal{C}}$ to $\operatorname{\mathcal{D}}_{E}$). The converse holds if $U$ is a cartesian fibration.

Proof. Apply Corollary 7.3.3.22 in the special case $\operatorname{\mathcal{E}}' = \{ E\} $. $\square$