Kerodon

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

Corollary 5.6.2.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets having essentially small fibers, 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$.