# Kerodon

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

Proposition 8.6.5.9. Let $\kappa$ be an uncountable regular cardinal, let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets which is essentially $\kappa$-small, and let $\operatorname{\mathcal{D}}$ be an $\infty$-category which is $\kappa$-cocomplete. Then the projection map $\pi : \operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) \rightarrow \operatorname{\mathcal{C}}$ is a cocartesian fibration of simplicial sets.

Proof. It follows from Corollary 5.3.6.8 that $\pi$ is a cartesian fibration of simplicial sets. Let $e: C \rightarrow C'$ be an edge of the simplicial set $\operatorname{\mathcal{C}}$, and let $e_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C'}$ be the functor given by covariant transport along $e$ (for the cocartesian fibration $U$). Then precomposition with $e_{!}$ determines a functor

$e^{\ast }: \{ C'\} \times _{\operatorname{\mathcal{C}}} \operatorname{Fun}(\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}) = \operatorname{Fun}( \operatorname{\mathcal{E}}_{C'}, \operatorname{\mathcal{D}}) \xrightarrow {\circ e_{!} } \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{D}}) = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{Fun}( \operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}, \operatorname{\mathcal{D}}).$

Proposition 5.3.6.9 guarantees that the functor $e^{\ast }$ is given by contravariant transport along $e$ (for the cartesian fibration $\pi$). Using Proposition 6.2.3.5, we see that $\pi$ is a cocartesian fibration if and only if the functor $e^{\ast }$ has a left adjoint (for every edge $e$ of $\operatorname{\mathcal{C}}$). By virtue of Corollary 7.3.6.3, it will suffice to show that every functor $F: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{D}}$ admits a left Kan extension along the functor $e_{!}: \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{C'}$. This is a special case of Proposition 7.6.7.13, by virtue of our assumptions on the cardinal $\kappa$. $\square$