Definition. Definable class in a fibration [frct-002W]
Definition. Definable class in a fibration [frct-002W]
Let \(E\) be a cartesian fibration over \(B\). A definable class \(\mathfrak {F}\) in \(E\) is a stable subcollection of the displayed objects of \(E\) such that for any \(\bar {u}\in E_{u}\), there exists a cartesian map \(\bar {v}\to \bar {u}\) lying over a monomorphism \(v\rightarrowtail u\) such that \(\bar {v}\in \mathfrak {F}\) and, moreover, any cartesian morphism \(\bar {w}\to \bar {u}\) such that \(\bar {w}\in \mathfrak {F}\) factors through \(\bar {v}\to \bar {u}\).