Adjusting the definition of a well-powered category to category theory with universes: size issues

Your dilemma can be resolved by Scott's trick, if your universes are cumulative von Neumann universes. Briefly, given an equivalence relation $E \subseteq C \times C$ on a class $C$ and $x \in C$, consider the (possibly proper) class $[x]'_E = \{y \in C \mid x E y\}$. Let $\alpha$ be the least ordinal such that $[x]'_E$ intersects $V_\alpha$, the set of all sets of rank at most $\alpha$. Now re-adjust the definition of equivalence class by defining it to be $[x]_E = [x]'_E \cap V_\alpha$. This way $[x]_E$ is set-sized and we have not relied on choice (but we did rely on regularity). The quotient $C/E$ may be defined as the class of all the set-sized equivalence classes $[x]_E$, for $x \in C$.

However, from a category-theoretic perspective, relying too heavily on particularities of a set-theoretic foundation is not such a good idea. One should look for definitions that are natural from the point of view of category theory, and then see how they play out in various settings.

The natural notion of equality in category theory is equivalence. Thus for many purposes it suffices to relax the condition of well-poweredness to the following. Given a category $C$ and an object $X$ in $C$, let $\mathrm{Mono}_C(X)$ be the (possibly large) preorder of all monos into $X$, seen as a category. Say that $C$ is essentially well-powered when for every $X$ the preorder $\mathrm{Mono}_C(X)$ is equivalent to a small category (in which case it is in fact equivalent to a small poset).

We are in familiar category-theoretic territory here. Analogously to the difference between "there existing products" and "having chosen products", we may further require there to be "chosen well-poweredness" by requiring a mapping $\mathrm{Sub} : \mathrm{ob}(C) \to \mathrm{Poset}$ which assigns to each object $X$ a (small) poset $\mathrm{Sub}(X)$ together with an equivalence $\mathrm{Set}(X) \simeq \mathrm{Mono}_C(X)$. (If $C$ has pullbacks one should think about turning $\mathrm{Sub}$ into a contravariant functor equivalent to the pullback (pseudo)functor.)

Notions of smallness and largeness appear outside traditional set theory, for instance in type theory and algebraic set theory. So the above definitions are not limited to set theory. It is "just a technicality" to figure out how one might get $\mathrm{Sub}$ in this or that setting. Maybe Scott's trick will save the day, or having some (large) choice, or Univalence axiom. As a category theorist one would just be used to looking around to see what's available. If some setting thinks that groups are not well-powered, well, tough luck. But most set theories will be able to accommodate moderate wishes for well-poweredness. (An interesting exception would be constructive set theory CZF.)

One simple way is to read the traditional definitions (à la Grothendieck, etc) but replacing existence conditions with chosen structure:

• A category $C$ is $U$-locally-small if it is equipped with a $U$-valued map $h : C_0 \times C_0 \to U$ and isomorphisms $h(x,y) \cong C(x,y)$. (Equivalently, a $U$-valued functor naturally isomorphic to the original hom-functor.)

• A category $C$ is $U$-well-powered if it is equipped with a map $S : C_0 \to U$, and isomorphisms $S(x) \cong \mathrm{Sub}(x)$. (Equivalently, a $U$-valued functor naturally iso to the original shbobject functor.)

• Both of these can be recovered just by reading the traditional definitions, but with a “$U$-small set” take to mean a set equipped with an isomorphism to some chosen element of $U$.

These are a fairly minimal tweak to the traditional definitions to make them non-choicy. They are easily seen to respect equivalence of categories, and also equivalence of universes (suitably defined); in this way, they are considerably more robust than the Borceux-style definition and similar ones. While these definitions do involve a choice of extra structure, this structure is in each case unique up to canonical isomorphism. This approach works analogously completely off-the-shelf for every smallness condition I know.

Borceux's Definition 4.1.1

An equivalence class of monomorphisms with codomain A is called a subobject of A.

in combination with Definition 4.1.2

A category A is well-powered when the subobjects of every object constitute a set.

and the subsequent claim that the category of sets is well-powered contradicts Axiom 1.1.7 in his book:

A class is a set if and only if it belongs to some (other) class.

A large category (meaning the collection of objects is a proper class) can have a proper equivalence class of subobjects, which cannot be an element of any set. So a contractible groupoid with a proper class of objects is not a well-powered category in this definition, even though it is equivalent to the terminal category, which is well-powered.

The problem arises from the fact that the definition of a quotient of classes using equivalence classes is only correct when each equivalence class is a set. Otherwise one must define quotients using universal properties.

Thus, this problem can be resolved by using a categorical definition of a quotient instead of a set-theoretical one:

A category C is well-powered if for any object A∈C there is a surjective map Sub(A)→Q such that two subobjects of A are mapped to the same element of Q if and only if they are isomorphic, and, additionally, Q is a set (or a U-small set, etc.).

(Categorically, we could also say that Q is the quotient of Sub(A) with respect to the equivalence relation of isomorphism, where the quotient is defined using a universal property as the initial object in the category of maps Sub(A)→Q that send isomorphic subobjects to equal elements, without any reference to equivalence classes.)

Then Scott's trick, as explained in Andrej Bauer's answer, shows that other (correct) definitions are equivalent to this one.