Type u is well-powered #
One would hope that for a particular concrete category
it's viable to prove
[WellPowered C] without explicitly aligning
with the "hand-rolled" definition of subobjects.
This may be possible using Lawvere theories, but it remains to be seen whether this just pushes lumps around in the carpet.