Definition. Cocartesian morphism [frct-0016]

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

We use a “pushout corner” to indicate \(\bar {x}\to \bar {y}\) as a cocartesian morphism, a notation justified by our discussion of the dual self-indexing.