Kerodon

Corollary 7.3.7.3. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be an exponentiable inner fibration of $\infty $-categories, let $\operatorname{\mathcal{D}}$ be an $\infty $-category, and let $\pi : \operatorname{Fun}(\operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{B}}$ be the projection map. Let $f: \operatorname{\mathcal{A}}\rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$ be a functor of $\infty $-categories and let $\operatorname{\mathcal{A}}^{0} \subseteq \operatorname{\mathcal{A}}$ be a full subcategory. If the induced map $\operatorname{\mathcal{A}}\times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is left Kan extended from $\operatorname{\mathcal{A}}^{0} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$, then $f$ is $\pi $-left Kan extended from $\operatorname{\mathcal{A}}^{0}$.