[0017] Definition 6.1·b (Cocartesian fibration).

A displayed category $E$ over $B$ is a cocartesian fibration when for each $f : x \to y\in B$ and $\bar{x}\in E\Sub{x}$, there exists a displayed object $\bar{y}\in E\Sub{y}$ and a cocartesian morphism $\bar{f} : \bar{x}\to\Sub{f} \bar{y}$.