Kerodon

Corollary 7.3.7.9. 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 $e$ be a morphism of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}})$, corresponding to a pair $( \overline{e}, f )$ where $\overline{e}$ is a morphism of $\operatorname{\mathcal{B}}$ and $f: \Delta ^1 \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ is a functor of $\infty $-categories. If $f$ is left Kan extended from $\{ 0\} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$, then the morphism $e$ is $\pi $-cocartesian.