$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Proposition 7.4.1.9. Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a left fibration of simplicial sets and let $\mathscr {F}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{S}}$ be a diagram. The following conditions are equivalent:
- $(1)$
The diagram $\mathscr {F}$ is a covariant transport representation for $U$, in the sense of Definition 5.6.5.1.
- $(2)$
There exists a natural transformation $\alpha : \underline{ \Delta ^{0} }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ which exhibits $\mathscr {F}$ as a covariant transport representation for $U$, in the sense of Definition 7.4.1.8.
- $(3)$
There exists an equivalence of $U$ with the left fibration $\{ \Delta ^0 \} \operatorname{\vec{\times }}_{\operatorname{\mathcal{S}}} \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{C}}$.
Proof.
Unwinding the definitions, we see that commutative diagrams
\[ \xymatrix { \operatorname{\mathcal{E}}\ar [dr]^{U} \ar [rr]^{T} & & \{ \Delta ^0 \} \operatorname{\vec{\times }}_{\operatorname{\mathcal{S}}} \operatorname{\mathcal{C}}\\ & \operatorname{\mathcal{C}}& } \]
can be identified with morphisms $\alpha : \underline{ \Delta ^{0} }_{\operatorname{\mathcal{E}}} \rightarrow \mathscr {F}|_{\operatorname{\mathcal{E}}}$ in the $\infty $-category $\operatorname{Fun}(\operatorname{\mathcal{E}}, \operatorname{\mathcal{S}})$. Under this identification, $T$ is an equivalence of left fibrations over $\operatorname{\mathcal{C}}$ if and only if $\alpha $ exhibits $\mathscr {F}$ as a covariant transport representation for $U$ (Corollary 5.1.7.16). This proves the equivalence $(2) \Leftrightarrow (3)$. The equivalence $(1) \Leftrightarrow (3)$ follows from the observation that the coslice diagonal
\[ \operatorname{\mathcal{S}}_{ \ast } = \operatorname{\mathcal{S}}_{ \Delta ^0 / } \hookrightarrow \{ \Delta ^0 \} \operatorname{\vec{\times }}_{\operatorname{\mathcal{S}}} \operatorname{\mathcal{S}} \]
is an equivalence of left fibrations over $\operatorname{\mathcal{S}}$ (Corollary 4.6.4.18).
$\square$