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

Equations

• MonTypeEquivalenceMon.monMonoid A = Monoid.mk ⋯ ⋯ npowRec ⋯ ⋯

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

Converting a monoid object in Type to a bundled monoid.

Equations

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

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

Converting a bundled monoid to a monoid object in Type.

Equations

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

noncomputable def monTypeEquivalenceMon : Mon_ (Type u) ≌ MonCat

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

Equations

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

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

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

Equations

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

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

Equations

• monTypeInhabited = { default := MonTypeEquivalenceMon.inverse.obj (MonCat.of PUnit.{u + 1} ) }

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

Equations

• CommMonTypeEquivalenceCommMon.commMonCommMonoid A = let __src := MonTypeEquivalenceMon.monMonoid A.toMon_; CommMonoid.mk ⋯

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

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

Equations

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

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

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

Equations

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

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.

Equations

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

noncomputable def commMonTypeEquivalenceCommMonForget : CommMonTypeEquivalenceCommMon.functor.comp (CategoryTheory.forget₂ CommMonCat MonCat) ≅ (CommMon_.forget₂Mon_ (Type u)).comp 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).

Equations

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

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

Equations

• commMonTypeInhabited = { default := CommMonTypeEquivalenceCommMon.inverse.obj (CommMonCat.of PUnit.{u + 1} ) }