# Kerodon

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

Corollary 7.4.3.15. Let $\operatorname{\mathcal{C}}$ be an $\infty$-category, let $\overline{U}: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{C}}^{\triangleright }$ be a cocartesian fibration, and set $\operatorname{\mathcal{E}}= \operatorname{\mathcal{C}}\times _{ \operatorname{\mathcal{C}}^{\triangleright } } \overline{\operatorname{\mathcal{E}}}$. Let $F: \overline{\operatorname{\mathcal{E}}} \rightarrow \operatorname{\mathcal{D}}$ be a functor of $\infty$-categories which carries $\overline{U}$-cocartesian morphisms of $\overline{\operatorname{\mathcal{E}}}$ to isomorphisms in $\operatorname{\mathcal{D}}$. If the covariant transport representation $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }: \operatorname{\mathcal{C}}^{\triangleright } \rightarrow \operatorname{\mathcal{QC}}$ is a colimit diagram, then $F$ is left Kan extended from $\operatorname{\mathcal{E}}$.

Proof. Combine the refraction criterion (Theorem 7.4.3.6) with Corollary 7.4.3.15, applied to the cocartesian fibration given by the composition

$\overline{\operatorname{\mathcal{E}}} \xrightarrow { \overline{U} } \operatorname{\mathcal{C}}^{\triangleright } \rightarrow (\Delta ^0)^{\triangleright } \simeq \Delta ^1.$
$\square$