Type u is well-powered #

By building a categorical equivalence MonoOver α ≌ 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 [WellPowered 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.

theorem Types.monoOverEquivalenceSet_inverse_map (α : Type u) {s : Set α} {t : Set α} (b : s t) :
(Types.monoOverEquivalenceSet α) b = CategoryTheory.MonoOver.homMk (fun (w : ((fun (s : Set α) =>' Subtype.val) s).obj.left) => w, )

The category of MonoOver α, for α : Type u, is equivalent to the partial order Set α.

  • One or more equations did not get rendered due to their size.
Instances For

    For α : Type u, Subobject α is order isomorphic to Set α.

    Instances For