Kerodon

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

Proposition 5.2.8.4. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of simplicial sets, and let $C$ and $D$ be vertices of $\operatorname{\mathcal{C}}$. Then:

  • There exists a morphism $F: \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ which is given by parametrized covariant transport.

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

Proof. Apply Lemma 5.2.2.13 to the simplicial set $K = \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C}$. $\square$