# Kerodon

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

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.

Proof. Apply Corollary 7.3.7.6 in the special case $\operatorname{\mathcal{E}}= \Delta ^0$. $\square$