Corollary [efr-8LGE]

Let p: \mathcal {D} \to \mathcal {C} be a fibration. Then there exists a category \mathcal {D}^\mathrm {fop}, called the fiberwise opposite of \mathcal {D}, whose objects are the same as \mathcal {D}, and where a morphism X \to Y is a tuple (f: p(X) \to p(Y), f^\#: f^*Y \to X \in \mathcal {D}_{p(X)}).