Kerodon

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

Proposition 5.2.2.4. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian 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}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ which is given by covariant transport along $f$.

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

Proof of Proposition 5.2.2.4. Apply Lemma 5.2.2.9 in the special case where $K$ is the $\infty $-category $\operatorname{\mathcal{E}}_{C}$, $H_0: K \rightarrow \operatorname{\mathcal{E}}$ is the inclusion map, and $\overline{H}$ is the composite map $\Delta ^1 \times K \rightarrow \Delta ^1 \xrightarrow {f} \operatorname{\mathcal{C}}$ (see Example 5.2.2.8). $\square$