$\Newextarrow{\xhookrightarrow}{10,10}{0x21AA}$
Corollary 8.4.2.7. Let $\operatorname{\mathcal{C}}$ be a locally $\kappa $-small $\infty $-category, let $U: \widetilde{\operatorname{\mathcal{C}}} \rightarrow \operatorname{\mathcal{C}}$ be a right fibration, and let $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{S}}^{< \kappa }$ be a functor. The following conditions are equivalent:
- $(1)$
The functor $\mathscr {F}$ is a covariant transport representation for the left fibration $U^{\operatorname{op}}: \widetilde{\operatorname{\mathcal{C}}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$.
- $(2)$
There exists a categorical pullback square
\[ \xymatrix@R =50pt@C=50pt{ \widetilde{\operatorname{\mathcal{C}}} \ar [d]^{U} \ar [r] \ar [d] & \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}^{< \kappa })_{ / \mathscr {F} } \ar [d] \\ \operatorname{\mathcal{C}}\ar [r]^-{h_{\bullet }} & \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}^{<\kappa } ), } \]
where $h_{\bullet }$ is a covariant Yoneda embedding for $\operatorname{\mathcal{C}}$.
Proof.
Choose a cardinal $\lambda \geq \kappa $ such that $\operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}^{< \kappa } )$ is locally $\lambda $-small, and let $H: \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}^{< \kappa } )^{\operatorname{op}} \rightarrow \operatorname{\mathcal{S}}^{< \lambda }$ be a functor represented by $\mathscr {F} \in \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}^{< \kappa } )$. It follows from Proposition 5.6.6.21 that $H$ is a covariant transport representation for the left fibration $(\operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}^{< \kappa } )_{ / \mathscr {F} })^{\operatorname{op}} \rightarrow \operatorname{Fun}( \operatorname{\mathcal{C}}^{\operatorname{op}}, \operatorname{\mathcal{S}}^{ < \kappa } )^{\operatorname{op}}$. Consequently, if condition $(2)$ is satisfied, then $H \circ h_{\bullet }^{\operatorname{op}}$ is a covariant transport representation for the left fibration $U^{\operatorname{op}}$. Proposition 8.4.2.5 implies that $H \circ h_{\bullet }^{\operatorname{op}}$ is isomorphic to $\mathscr {F}$. This proves the implication $(2) \Rightarrow (1)$, and the reverse implication follows from the fact that the equivalence class of a left fibration is determined by its covariant transport representation (Corollary 5.6.0.6).
$\square$