# 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)`

.

- subobject_small : ∀ (X : C), Small.{v, max u₁ v} (CategoryTheory.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`

.

## Instances

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