Suppose that \(E\) is a right fibration over \(B\), and fix \(b\in B\),
\(\bar {b}\in E_{b}\), and a vertical map \(f:\bar {b}\xrightarrow [1_{b}]{} \bar {b}\).
Using the hypothesis that \(f\) is cartesian, it has a unique section
\(g:\bar {b}\xrightarrow [1_{b}]{} \bar {b}\) as follows:
Likewise, because \(g\) is cartesian, \(f\) is the unique section of \(g\); thus \(f\) is an
isomorphism in \(E_{b}\).
Conversely, suppose that \(E\) is a cartesian fibration whose vertical maps are
isomorphisms. Fix \(f:x\to y \in B\) and an arbitrary displayed morphism
\(\bar {g}:\bar {x}\xrightarrow [f]{}\bar {y}\). Then \(\bar {g}\) is the precomposition of a
cartesian lift \(\bar {f}:\bar {x}'\xrightarrow [f]{}\bar {y}\) with a vertical map:
Because vertical maps are isomorphisms and \(\bar {f}\) is cartesian, we can observe that \(\bar {g}\) is cartesian as follows, writing \(\bar {m} : \bar {u}\xrightarrow [m]{} \bar {x}'\) for the unique factorization of \(\bar {h}\) through \(\bar {f}\) over \(m\):
