Kerodon

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

Construction 5.2.8.9 (Enriched Homotopy Transport: Covariant Case). Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a cocartesian fibration of $\infty $-categories and let us regard the homotopy category $\mathrm{h} \mathit{\operatorname{\mathcal{C}}}$ as enriched over the homotopy category $\mathrm{h} \mathit{\operatorname{Kan}}$ of Kan complexes (Construction 4.6.8.13). It follows from Proposition 5.2.8.8 (and Example 5.2.2.5) that there is a unique $\mathrm{h} \mathit{\operatorname{Kan}}$-enriched functor $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ with the following properties:

  • For each object $C$ of the $\infty $-category $\operatorname{\mathcal{C}}$, $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}(C)$ is the $\infty $-category $\operatorname{\mathcal{E}}_{C} = \{ C\} \times _{\operatorname{\mathcal{C}}} \operatorname{\mathcal{E}}$ (regarded as an object of $\mathrm{h} \mathit{\operatorname{QCat}}$).

  • For every pair of objects $C,D \in \operatorname{\mathcal{C}}$, the induced map

    \[ \operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \rightarrow \operatorname{Fun}( \operatorname{\mathcal{E}}_{C}, \operatorname{\mathcal{E}}_{D} )^{\simeq } \]

    in $\mathrm{h} \mathit{\operatorname{Kan}}$ corresponds to the parametrized covariant transport functor $\operatorname{Hom}_{\operatorname{\mathcal{C}}}(C,D) \times \operatorname{\mathcal{E}}_{C} \rightarrow \operatorname{\mathcal{E}}_{D}$ of supplied by Proposition 5.2.8.4 (which is well-defined up to isomorphis).

We will refer to $\operatorname{hTr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}$ as the enriched homotopy transport representation of the cocartesian fibration $U$. Note that the underlying functor of ordinary categories $\mathrm{h} \mathit{\operatorname{\mathcal{C}}} \rightarrow \mathrm{h} \mathit{\operatorname{QCat}}$ coincides with homotopy transport representation of Construction 5.2.5.2.