Kerodon

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

Proposition 5.2.2.16. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cartesian fibration of simplicial sets and let $f: C \rightarrow D$ be an edge of $\operatorname{\mathcal{C}}$. Then:

  • There exists a functor $F: \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ which is given by contravariant transport along $f$.

  • An arbitrary functor $F': \operatorname{\mathcal{E}}_{D} \rightarrow \operatorname{\mathcal{E}}_{C}$ is given by contravariant transport along $f$ if and only if it is isomorphic to $F$ (as an object of the $\infty $-category $\operatorname{Fun}( \operatorname{\mathcal{E}}_{D}, \operatorname{\mathcal{E}}_{C} )$).