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 => { val := w, property := (_ : w t) }
theorem Types.monoOverEquivalenceSet_functor_map (α : Type u) {f : CategoryTheory.MonoOver α} {g : CategoryTheory.MonoOver α} (t : f g) :
(Types.monoOverEquivalenceSet α) t = CategoryTheory.homOfLE (_ : ∀ ⦃a : α⦄, a (fun f => Set.range f.obj.hom) fa (fun f => Set.range f.obj.hom) g)

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

Instances For

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

    Instances For