[002C] Lemma 2.3·b (Hypocartesian = cartesian in a cartesian fibration).

Let $E$ be a cartesian fibration in the sense of Definition 2·c [0002], and let $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$ be displayed over $f:x\to y$. The displayed morphism $\bar{f}$ is cartesian if and only if it is hypocartesian.

Proof. Any cartesian map is clearly hypocartesian. To see that a hypocartesian map $\bar{f}:\bar{x}\to\Sub{f}\bar{y}$ in a cartesian fibration is cartesian, we consider the cartesian lift of $f:x\to y$ under $\bar{y}$:

As the cartesian lift $\bar{x}\tick\to \bar{y}$ is also hypocartesian, it follows that there is a unique vertical isomorphism identifying $\bar{x}$ with $\bar{x}\tick$ factoring $\bar{f} : \bar{x}\to\Sub{f}\bar{y}$ through $\bar{f}\tick : \bar{x}\tick\to\Sub{f}\bar{y}$. Being cartesian over $f$ is clearly stable under isomorphism, hence we conclude that $\bar{f}$ is cartesian from the fact that $\bar{f}\tick$ is cartesian.