Corollary 7.4.3.17. 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. Let $\mathrm{Rf}: \operatorname{\mathcal{E}}\rightarrow \overline{\operatorname{\mathcal{E}}}_{{\bf 1} }$ be a covariant refraction diagram, so that there exists a natural transformation $h: \operatorname{id}_{\operatorname{\mathcal{E}}} \rightarrow \mathrm{Rf}$ (in the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}, \overline{\operatorname{\mathcal{E}}} )$) which carries each object $X \in \operatorname{\mathcal{E}}$ to an $\overline{U}$-cocartesian morphism $h_{X}: X \rightarrow \mathrm{Rf}(X)$. Our assumption that $\operatorname{Tr}_{ \overline{\operatorname{\mathcal{E}}} / \operatorname{\mathcal{C}}^{\triangleright } }$ is a colimit diagram guarantees that the functor $\mathrm{Rf}$ exhibits $\overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }$ as a localization of $\operatorname{\mathcal{E}}$ (Corollary 7.4.3.9). Moreover, for each object $X \in \operatorname{\mathcal{C}}$, the functor $F$ carries $h_{X}$ to an isomorphism in the $\infty $-category $\operatorname{\mathcal{D}}$. Set $F_0 = F|_{\operatorname{\mathcal{E}}}$ and $F_1 = F|_{ \overline{\operatorname{\mathcal{E}}}_{ {\bf 1} }}$. Applying Proposition 7.3.1.17, we deduce that the natural transformation $F(h): F_0 \rightarrow F_1 \circ \mathrm{Rf}$ exhibits the functor $F_1$ as a left Kan extension of $F_0$ along $\mathrm{Rf}$. By virtue of Example 7.4.3.4, the natural transformation $h$ exhibits $\mathrm{Rf}$ as a covariant transport functor for the cocartesian fibration
Applying Corollary 7.3.2.14, we conclude that the functor $F$ is left Kan extended from $\operatorname{\mathcal{E}}$. $\square$