Kerodon

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

Proposition 5.3.2.11. Let $q: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{D}}$ be a locally cocartesian fibration of simplicial sets and let $e: X \rightarrow Y$ be an edge of $\operatorname{\mathcal{D}}$. Then there exists a functor $F: \operatorname{\mathcal{C}}_{X} \rightarrow \operatorname{\mathcal{C}}_{Y}$ which is given by covariant transport along $e$. Moreover, an arbitrary functor $F': \operatorname{\mathcal{C}}_{X} \rightarrow \operatorname{\mathcal{C}}_{Y}$ is given by covariant transport along $e$ if and only if it is isomorphic to $F$ (as an object of the $\infty $-category of functors $\operatorname{Fun}( \operatorname{\mathcal{C}}_{X}, \operatorname{\mathcal{C}}_{Y} )$).