Kerodon

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

Definition 5.2.8.1 (Parametrized Covariant Transport). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be cocartesian fibration of simplicial sets, and let $C$ and $D$ be vertices of $\operatorname{\mathcal{C}}$. We will say that a morphism $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 there exists a morphism of simplicial sets $\widetilde{F}: \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_ C \rightarrow \operatorname{\mathcal{E}}$ satisfying the following conditions:

$(1)$

The diagram of simplicial sets

\[ \xymatrix@R =50pt@C=50pt{ \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \ar [r]^-{ \widetilde{F} } \ar [d] & \operatorname{\mathcal{E}}\ar [d]^-{U} \\ \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \ar [r] & \operatorname{\mathcal{C}}} \]

commutes (where the lower horizontal map is induced by the inclusion $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \hookrightarrow \operatorname{Fun}(\Delta ^1, \operatorname{\mathcal{C}})$).

$(2)$

The restriction $\widetilde{F}|_{ \{ 0\} \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C}}$ is given by projection onto $\operatorname{\mathcal{E}}_{C}$, and the restriction $\widetilde{F}|_{ \{ 1\} \times C^{\ast }(\operatorname{\mathcal{E}}) }$ is equal to $F$.

$(3)$

For every edge $f: C \rightarrow D$ of $\operatorname{\mathcal{C}}$ and every object $X \in \operatorname{\mathcal{E}}_{C}$, the composite map

\[ \Delta ^1 \times \{ f\} \times \{ X\} \hookrightarrow \Delta ^1 \times \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_ C \xrightarrow { \widetilde{F} } \operatorname{\mathcal{E}} \]

is a $U$-cocartesian edge of $\operatorname{\mathcal{E}}$.

If these conditions are satisfied, we say that the morphism $\widetilde{F}$ witnesses $F$ as given by parametrized covariant transport.