Suppose first that \(E\) is a cartesian fibration in our sense. Then
\(E\) has hypocartesian lifts because it has cartesian lifts. For closure under composition, fix hypocartesian \(\bar {f},\bar {g}\); because hypocartesian and cartesian maps coincide in a cartesian fibration generalized pullback lemma
Conversely, suppose that \(E\) is a cartesian fibration in the sense of Grothendieck, and let \(\bar {f}:\bar {x}\xrightarrow [f]{}\bar {y}\) be the hypocartesian lift of \(f:x\to y\) at \(\bar {y}\in E_{y}\); we shall see that \(\bar {f}\) is also a cartesian lift of \(f\) at \(\bar {y}\) by constructing a unique factorization as follows:
Let \(\bar {m}:\bar {u}'\xrightarrow [m]{}\bar {x}\) be the hypocartesian lift of \(m\) at \(\bar {x}\), where \(\bar {u}'\in E_{u}\). By hypothesis, the composite \(\bar {m};\bar {f} : \bar {u}'\xrightarrow [m;f]{}\bar {y}\) is hypocartesian, so \(\bar {h}\) factors uniquely through \(\bar {m};\bar {f}\) over \(1_{u}\):
The composite \(i;\bar {m} : \bar {u}\xrightarrow [m]{}\bar {x}\) is the required (cartesian) factorization of \(\bar {h}\) through \(\bar {f}\) over \(m\). To see that \(i;\bar {m}\) is the unique such map, we observe that all morphisms \(\bar {u}\xrightarrow [m]{}\bar {x}\) factor uniquely through \(\bar {m}\) over \(1_{u}\) as a consequence of \(\bar {m}\) being hypocartesian.
