Kerodon

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

Remark 8.4.0.18. For historical reasons, it is traditional to place more emphasis on the duals of the notions introduced above. We say that a functor of categories $U: \operatorname{\mathcal{E}}\rightarrow \operatorname{\mathcal{C}}$ is a cartesian fibration (fibration in sets, fibration in groupoids) if the opposite functor $U^{\operatorname{op}}: \operatorname{\mathcal{E}}^{\operatorname{op}} \rightarrow \operatorname{\mathcal{C}}^{\operatorname{op}}$ is a cocartesian fibration (opfibration in sets, opfibration in groupoids). If $U$ is a cartesian fibration, then there exists a functor of $2$-categories $\mathscr {F}: \operatorname{\mathcal{C}}^{\operatorname{op}} \rightarrow \mathbf{Cat}$ and an isomorphism of $\operatorname{\mathcal{E}}$ with the category $\int ^{\operatorname{\mathcal{C}}} \mathscr {F}$, characterized by the formula $(\int ^{\operatorname{\mathcal{C}}} \mathscr {F})^{\operatorname{op}} = \int _{\operatorname{\mathcal{C}}^{\operatorname{op}}} \mathscr {F}^{\operatorname{op}}$ (see Remark 5.5.2.5).