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$.

[0021] Corollary 2.6.2·a.

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$: