2.6.2. Cartesian lifts in the opposite category [000U]
The foregoing characterization of cartesian maps in $\OpCat{E}$ immediately implies that $\OpCat{E}$ is fibered over $B$.
The displayed category $\OpCat{E}$ is a cartesian fibration.
Proof.
Fixing $\bar{y}\in \OpCat{E}\Sub{y}$ and $f:x\to y\in B$, we must
exhibit a cartesian lift $\bar{f} : \bar{x}\to\Sub{f}\bar{y}\in \OpCat{E}$.
By the characterization [000T] it suffices to find any map over $f$ whose vertical component is an isomorphism. Writing $\bar{y}\Sub{x}\to\Sub{f}\bar{y}$ for the cartesian lift of $f$ in $E$, consider the map in $\OpCat{E}$ presented by the following span in $E$:
∎