[0001] Definition 2·b (Cartesian morphisms).

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 cartesian over $f$ when for any $m:u\to x$ and $\bar{h}:\bar{u}\to\Sub{m;f} \bar{y}$ there exists a unique $\bar{m} : \bar{u}\to\Sub{m} \bar{x}$ with $\bar{m};\bar{f} = \bar{h}$. We visualize this unique factorization of $\bar{h}$ through $\bar{f}$ over $m$ as follows:

Above we have used the “pullback corner” to indicate $\bar{x}\to\bar{y}$ as a cartesian map. We return to this in our discussion of the self-indexing [0003] of a category.