Definition. Cartesian fibration [frct-0002]

A displayed category \(E\) over \(B\) is said to be a cartesian fibration, when for each morphism \({x}\xrightarrow {{f}}{y}\) and displayed object \(\bar {y}\in E_{y}\), there exists a displayed object \(\bar {x}\in E_{x}\) and a cartesian morphism \({\bar {x}}\xrightarrow [f]{\bar {f}}{\bar {y}}\). Note that the pair \((\bar {x},\bar {f})\) is unique up to unique isomorphism, so being a cartesian fibration is a property of a displayed category.

We will also refer to cartesian fibrations as simply fibrations or fibered categories.

There are other variations of fibration. For instance, \(E\) is said to be an isofibration when the condition above holds just for isomorphisms \(f : x\cong y\) in the base.