Mon_ (Type u) ≌ MonCat.{u}

The category of internal monoid objects in Type is equivalent to the category of "native" bundled monoids.

Moreover, this equivalence is compatible with the forgetful functors to Type.

instance MonTypeEquivalenceMon.monMonoid (A : Mon_ (Type u)) : Monoid A.X

noncomputable def MonTypeEquivalenceMon.functor : CategoryTheory.Functor (Mon_ (Type u)) MonCat

Converting a monoid object in Type to a bundled monoid.

noncomputable def MonTypeEquivalenceMon.inverse : CategoryTheory.Functor MonCat (Mon_ (Type u))

Converting a bundled monoid to a monoid object in Type.

noncomputable def monTypeEquivalenceMon : Mon_ (Type u) ≌ MonCat

The category of internal monoid objects in Type is equivalent to the category of "native" bundled monoids.

noncomputable def monTypeEquivalenceMonForget : CategoryTheory.Functor.comp MonTypeEquivalenceMon.functor (CategoryTheory.forget MonCat) ≅ Mon_.forget (Type u)

The equivalence Mon_ (Type u) ≌ MonCat.{u} is naturally compatible with the forgetful functors to Type u.

noncomputable instance monTypeInhabited : Inhabited (Mon_ (Type u))

instance CommMonTypeEquivalenceCommMon.commMonCommMonoid (A : CommMon_ (Type u)) : CommMonoid A.X

noncomputable def CommMonTypeEquivalenceCommMon.functor : CategoryTheory.Functor (CommMon_ (Type u)) CommMonCat

Converting a commutative monoid object in Type to a bundled commutative monoid.

noncomputable def CommMonTypeEquivalenceCommMon.inverse : CategoryTheory.Functor CommMonCat (CommMon_ (Type u))

Converting a bundled commutative monoid to a commutative monoid object in Type.

noncomputable def commMonTypeEquivalenceCommMon : CommMon_ (Type u) ≌ CommMonCat

The category of internal commutative monoid objects in Type is equivalent to the category of "native" bundled commutative monoids.

noncomputable def commMonTypeEquivalenceCommMonForget : CategoryTheory.Functor.comp CommMonTypeEquivalenceCommMon.functor (CategoryTheory.forget₂ CommMonCat MonCat) ≅ CategoryTheory.Functor.comp (CommMon_.forget₂Mon_ (Type u)) MonTypeEquivalenceMon.functor

The equivalences Mon_ (Type u) ≌ MonCat.{u} and CommMon_ (Type u) ≌ CommMonCat.{u} are naturally compatible with the forgetful functors to MonCat and Mon_ (Type u).

noncomputable instance commMonTypeInhabited : Inhabited (CommMon_ (Type u))