4.4.2. Bénabou's notion of definability [002S]

We will now construe Section 4.4.1 [002Q] as the instantiation at the canonical self-indexing $\SelfIx{\mathscr{M}}$ of a more general notion of definability for classes of objects in a cartesian fibration, defined forthwith. The following definition of definability in a cartesian fibration is due to Bénabou, but is discussed in print by Borceux (Handbook of Categorical Algebra 2 – Categories and Structures, 1994), Jacobs (Categorical Logic and Type Theory, 1999), Streicher (Fibred Categories à La Jean Bénabou, 2018).

[002W] Definition 4.4.2·a (Definable class in a fibration).

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\Sub{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}$.

[002O] Remark 4.4.2·b.

Let $\mathscr{M}$ be a model of ETCS; and let $\mathfrak{C}$ be a class of families of sets in $\mathscr{M}$. Then $\mathfrak{C}$ is a class of objects in the canonical self-indexing $\SelfIx{\mathscr{M}}$ over $\mathscr{M}$. Furthermore, $\mathscr{M}$ a definable class in $\SelfIx{\mathscr{M}}$ in the sense of Definition 4.4.2·a [002W] if and only if it is a definable class of families of sets in the sense of Definition 4.4.1·c [002P].