# 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.

@[simp]
theorem Types.monoOverEquivalenceSet_inverse_obj (α : Type u) (s : Set α) :
.inverse.obj s = CategoryTheory.MonoOver.mk' Subtype.val
@[simp]
theorem Types.monoOverEquivalenceSet_counitIso (α : Type u) :
.counitIso = CategoryTheory.NatIso.ofComponents (fun (s : Set α) => )
@[simp]
theorem Types.monoOverEquivalenceSet_functor_obj (α : Type u) (f : ) :
.functor.obj f = Set.range f.obj.hom
@[simp]
theorem Types.monoOverEquivalenceSet_functor_map (α : Type u) {f : } {g : } (t : f g) :
.functor.map t =
@[simp]
theorem Types.monoOverEquivalenceSet_inverse_map (α : Type u) {s : Set α} {t : Set α} (b : s t) :
.inverse.map b = CategoryTheory.MonoOver.homMk (fun (w : ((fun (s : Set α) => CategoryTheory.MonoOver.mk' Subtype.val) s).obj.left) => w, )
@[simp]
noncomputable def Types.monoOverEquivalenceSet (α : Type u) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
noncomputable def Types.subobjectEquivSet (α : Type u) :

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

Equations
• = .thinSkeletonOrderIso
Instances For