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}$:
