Kerodon

Corollary 5.6.5.13. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be an essentially small cocartesian fibration of simplicial sets, let $\operatorname{\mathcal{C}}' \subseteq \operatorname{\mathcal{C}}$ be a simplicial subset, and let $\mathscr {F}': \operatorname{\mathcal{C}}' \rightarrow \operatorname{\mathcal{QC}}$ be a covariant transport representation for the projection map $\operatorname{\mathcal{C}}' \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}'$. Then there exists a morphism $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}$ satisfying $\mathscr {F}' = \mathscr {F}|_{\operatorname{\mathcal{C}}'}$ which is a covariant transport representation of $U$.