Kerodon

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

Variant 8.6.8.4. It will sometimes be useful to apply Definition 8.6.8.1 to cartesian fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ which are not essentially small. Let $\kappa $ be an uncountable cardinal. We say that a diagram $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{QC}}^{< \kappa }$ is a contravariant transport representation for $U$ if $U$ is cartesian conjugate to the cocartesian fibration $\int _{\operatorname{\mathcal{C}}} \mathscr {F} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$. Such a diagram exists if and only if the cartesian fibration $U$ is essentially $\kappa $-small, in which case it is uniquely determined up to isomorphism. Moreover, the formation of contravariant transport representations induces a bijection

\[ \xymatrix { \textnormal{Essentially $\kappa $-small cartesian fibrations $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$} \} / \textnormal{Equivalence} \ar [d] \\ \{ \textnormal{Diagrams $\operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{QC}}^{< \kappa }$} \} / \textnormal{Isomorphism}. } \]