Definition [efr-Z7EF]

Let p: \mathcal {D} \to \mathcal {C} be a functor. Given X \in \mathcal {C}, write \mathcal {D}_X for the (strict) pullback \{x\} \times _\mathcal {C} \mathcal {D}. Explicitly, this consists of the objects in \mathcal {D} with p(A) = X and the morphisms with p(f) = 1_X.

Let f: X \to Y \in \mathcal {C} be a morphism.

1. A map \bar {f}: \bar {X} \to \bar {Y} with p(\bar {f}) = f is locally Cartesian if for each \bar {X}' with p(\bar {X}') = X, postcomposition with \bar {f} induces a bijection \{g: \bar {X}' \to \bar {X} \mid p(g) = 1_X\} \xrightarrow {\sim } \{g' : \bar {X'} \to \bar {Y} \mid p(g') = f\}
2. A map is Cartesian if for every g: Z \to X and \bar {Z} with p(\bar {Z}) = Z, there is a bijection \{\bar {g} : \bar {Z} \to \bar {X} \mid p(\bar {g}) = g\} \to \{\bar {g}' : \bar {Z} \to \bar {Y} \mid p(\bar {g'} = fg)\}, note that every Cartesian map is locally Cartesian (take g = 1_X)
3. p is a Grothendieck fibration (or just fibration) if, for every \bar {Y} \in \mathcal {D} such that p(\bar {Y}) = Y, there exists a Cartesian map \bar {f}: \bar {X} \to \bar {Y} (for some \bar {Y}) so that p(\bar {f}) = f