Well-powered categories #

A category (C : Type u) [Category.{v} C] is [WellPowered C] if for every X : C, we have Small.{v} (Subobject X).

(Note that in this situation Subobject X : Type (max u v), so this is a nontrivial condition for large categories, but automatic for small categories.)

This is equivalent to the category MonoOver X being EssentiallySmall.{v} for all X : C.

When a category is well-powered, you can obtain nonconstructive witnesses as Shrink (Subobject X) : Type v and equivShrink (Subobject X) : Subobject X ≃ Shrink (subobject X).

A category (with morphisms in Type v) is well-powered if Subobject X is v-small for every X.

We show in wellPowered_of_essentiallySmall_monoOver and essentiallySmall_monoOver that this is the case if and only if MonoOver X is v-essentially small for every X.


    Being well-powered is preserved by equivalences, as long as the two categories involved have their morphisms in the same universe.