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 subtype_val_mono {α : Type u} (s : Set α) : CategoryTheory.Mono (CategoryTheory.asHom Subtype.val)

@[simp]

theorem Types.monoOverEquivalenceSet_inverse_obj (α : Type u) (s : Set α) : (Types.monoOverEquivalenceSet α).inverse.obj s = CategoryTheory.MonoOver.mk' Subtype.val

@[simp]

theorem Types.monoOverEquivalenceSet_counitIso (α : Type u) : (Types.monoOverEquivalenceSet α).counitIso = CategoryTheory.NatIso.ofComponents fun s => CategoryTheory.eqToIso (_ : Set.range Subtype.val = s)

@[simp]

theorem Types.monoOverEquivalenceSet_inverse_map (α : Type u) {s : Set α} {t : Set α} (b : s ⟶ t) : (Types.monoOverEquivalenceSet α).inverse.map b = CategoryTheory.MonoOver.homMk fun w => { val := ↑w, property := (_ : ↑w ∈ t) }

@[simp]

theorem Types.monoOverEquivalenceSet_functor_obj (α : Type u) (f : CategoryTheory.MonoOver α) : (Types.monoOverEquivalenceSet α).functor.obj f = Set.range f.obj.hom

@[simp]

theorem Types.monoOverEquivalenceSet_functor_map (α : Type u) {f : CategoryTheory.MonoOver α} {g : CategoryTheory.MonoOver α} (t : f ⟶ g) : (Types.monoOverEquivalenceSet α).functor.map t = CategoryTheory.homOfLE (_ : ∀ ⦃a : α⦄, a ∈ (fun f => Set.range f.obj.hom) f → a ∈ (fun f => Set.range f.obj.hom) g)

@[simp]

theorem Types.monoOverEquivalenceSet_unitIso (α : Type u) : (Types.monoOverEquivalenceSet α).unitIso = CategoryTheory.NatIso.ofComponents fun f => CategoryTheory.MonoOver.isoMk (Equiv.toIso (Equiv.ofInjective f.obj.hom (_ : Function.Injective f.obj.hom)))

noncomputable def Types.monoOverEquivalenceSet (α : Type u) : CategoryTheory.MonoOver α ≌ Set α

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

instance instWellPoweredTypeTypes : CategoryTheory.WellPowered (Type u)

noncomputable def Types.subobjectEquivSet (α : Type u) : CategoryTheory.Subobject α ≃o Set α

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