Well-Powered Category

A category $C$ is well-powered if for every $A:C_{0}$, the subobjects of $A$ form a set.

There are a couple of ways of interpreting this definition in type-theoretic foundations:

• As an essential smallness condition on $\mathrm{Sub}(A)$.
• As a completeness condition on $\mathrm{Sub}(A)$
• As a H-Level restriction on the fibration $\mathrm{Sub}(A)$.

However, I think the morally correct answer comes from this mathoverflow answer: what we want is a comprehension-category like structure that picks monos as structure. Taylor takes this approach in “Well Founded Coalgebras and Recursion”, and cites “Abstract Families and the Adjoint Functor Theorems” as the main source of inspiration. Johnstone also gives a fibration-based definition in the Elephant; see B1.3.14. Streicher also gives a defitionn in Fibered Categories a La Jean Benabou.

Taylor advocates using a definition based off of generic objects.