mathlib documentation

category_theory.subobject.types

Type u is well-powered #

By building a categorical equivalence mono_over α ≌ set α for any α : Type u, we deduce that subobject α ≃o set α and that Type u is well-powered.

One would hope that for a particular concrete category C (AddCommGroup, etc) it's viable to prove [well_powered C] without explicitly aligning subobject X 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.

noncomputable def types.subobject_equiv_set (α : Type u) :

For α : Type u, subobject α is order isomorphic to set α.

Equations