Kerodon

Corollary 7.3.7.6. Let $U: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{B}}$ be an exponentiable inner fibration of $\infty $-categories, let $V: \operatorname{\mathcal{D}}\rightarrow \operatorname{\mathcal{E}}$ be an isofibration of $\infty $-categories, and let $V': \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}/\operatorname{\mathcal{B}}, \operatorname{\mathcal{E}})$ be the isofibration given by postcomposition with $V$ (see Proposition 4.5.9.18). 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 $V$-left Kan extended from $\{ 0\} \times _{\operatorname{\mathcal{B}}} \operatorname{\mathcal{C}}$, then the morphism $e$ is $V'$-cocartesian.