Kerodon

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

Corollary 9.5.3.9. There is an equivalence of $\infty $-categories

\[ \Psi : (\operatorname{\mathcal{QC}}^{\operatorname{LPr}} )^{\operatorname{op}} \rightarrow \operatorname{\mathcal{QC}}^{\operatorname{RPr}}, \]

which is characterized up to isomorphism by the following requirement:

  • Let $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ be a presentable cocartesian fibration with covariant transport representation $\operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}: \operatorname{\mathcal{C}}\rightarrow \operatorname{\mathcal{QC}}^{\operatorname{LPr}}$. Then the composition

    \[ \operatorname{\mathcal{C}}^{\operatorname{op}} \xrightarrow { \operatorname{Tr}_{\operatorname{\mathcal{E}}/\operatorname{\mathcal{C}}}^{\operatorname{op}} } ( \operatorname{\mathcal{QC}}^{\operatorname{LPr}} )^{\operatorname{op}} \xrightarrow {\Psi } \operatorname{\mathcal{QC}}^{\operatorname{RPr}} \]

    is a contravariant transport representation of $U$ (regarded as a cartesian fibration).