[0016] Definition 6.1·a (Cocartesian morphism).

Let $E$ be displayed over $B$, and let $f:x\to y \in B$; a morphism $\bar{f}:\bar{x}\to\Sub{f} \bar{y}$ in $E$ is called cocartesian over $f$ when for any $m:y\to u$ and $\bar{h}:\bar{x}\to\Sub{f;m} \bar{u}$ there exists a unique $\bar{m} : \bar{y}\to\Sub{m} \bar{u}$ with $\bar{f};\bar{m} = \bar{h}$: