[0002] Definition 2·c (Cartesian fibration).

A displayed category $E$ over $B$ is said to be a cartesian fibration, when for each morphism $f : x \to y$ and displayed object $\bar{y}\in E\Sub{y}$, there exists a displayed object $\bar{x}\in E\Sub{x}$ and a cartesian morphism $\bar{f} : \bar{x}\to\Sub{f} \bar{y}$ in the sense of Definition 2·b [0001]. Note that the pair $(\bar{x},\bar{f})$ is unique up to unique isomorphism, so being a cartesian fibration is a property of a displayed category.

There are other variations of fibration. For instance, $E$ is said to be an isofibration when the condition above holds just for isomorphisms $f : x \cong y$ in the base.