4.2.1. Generic objects [000K]

Up to equivalence of categories, we may detect global smallness of a category $C$ from the perspective of the family fibration $\FAM{C}$ (Section 2.7 [0006]). In particular, a category is equivalent to a globally small category when its family fibration has a generic object in the following sense.

[001E] Definition 4.2.1·a (Generic object).

Let $E$ be a cartesian fibration over $B$; a generic object for $E$ is defined to be an object $\bar{u}\in \TotCat{E}$ such that for any $\bar{z}\in \TotCat{E}$ there exists a cartesian map $\bar{z}\to \bar{u}$.

Warning. Our terminology differs from that of Jacobs (Categorical Logic and Type Theory, 1999); what we refer to as a generic object here is Jacobs’ weak generic object. We prefer the unqualified terminology, as generic objects in the stronger sense are very rare.

[000L] Theorem 4.2.1·b (Globally small categories).

An ordinary category $C$ is equivalent to a globally small category if and only if the fibration $\FAM{C}$ has a generic object.

Proof. To see that this is the case, suppose that $C$ has a set of objects. Then $C\in\SET$ and we define $\lfloor{C}\rfloor$ to be the displayed object $\brc{x}\Sub{x\in C}\in \FAM{C}[C]$. Fixing $I\in \SET$ and $z\in C^I$, we consider the cartesian map displayed over $z : I \to C$:

Conversely assume that $\FAM{C}$ has a generic object $\bar{u}\in\FAM{C}[U]$ for some $U\in \SET$; then we may equip $U$ with the structure of a globally small category such that $U$ is equivalent to $C$, using a construction that is similar to our implementation of the opposite fibration (Section 2.6 [000Q]). In particular we define a morphism $x\to y\in U$ to be given by the following data:

  1. a cartesian map $a\to\Sub{x} \bar{u}$ over $x : 1\to U$,
  2. a cartesian map $b\to\Sub{y} \bar{u}$ over $y : 1\to U$,
  3. and a vertical map $h:a\to b$ in $\FAM{C}[1]\simeq C$,

such that $(a\Sub{1},b\Sub{1},h\Sub{1})$ is identified with $(a\Sub{2},b\Sub{2},h\Sub{2})$ when $h_1$ and $h_2$ are equal modulo the (unique) vertical isomorphisms between the cartesian lifts in the sense depicted below:

Remember that a cartesian map $a\to\Sub{x}\bar{u}$ is standing for a choice of an object of $C$ encoded by $x\in U$. Because such choices are unique only up to isomorphism, we must include them explicitly in the data.