Kerodon

Proposition 7.4.2.13 (Covariant Transport as a Kan Extension). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small left fibration of $\infty $-categories, let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be a functor, and let $\alpha : \underline{ \Delta ^0 }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ be a natural transformation. Then $\alpha $ exhibits $\mathscr {F}$ as covariant transport representation for $U$ (in the sense of Definition 7.4.1.8) if and only if it exhibits $\mathscr {F}$ as a left Kan extension of $\underline{ \Delta ^0}_{\operatorname{\mathcal{E}}}$ along $U$ (in the sense of Variant 7.3.1.5).