Kerodon

Remark 11.5.0.99. 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.6.1.6).