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.

@[implicit_reducible]

instance MonTypeEquivalenceMon.monMonoid (A : Type u) [CategoryTheory.MonObj A] : Monoid A

Equations

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

noncomputable def MonTypeEquivalenceMon.functor : CategoryTheory.Functor (CategoryTheory.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 (CategoryTheory.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 : CategoryTheory.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) ≅ CategoryTheory.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.

@[implicit_reducible]

noncomputable instance monTypeInhabited : Inhabited (CategoryTheory.Mon (Type u))

Equations

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

@[implicit_reducible]

instance CommMonTypeEquivalenceCommMon.commMonCommMonoid (A : Type u) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] : CommMonoid A

Equations

• CommMonTypeEquivalenceCommMon.commMonCommMonoid A = { toMonoid := MonTypeEquivalenceMon.monMonoid A, mul_comm := ⋯ }

noncomputable def CommMonTypeEquivalenceCommMon.functor : CategoryTheory.Functor (CategoryTheory.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 (CategoryTheory.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 : CategoryTheory.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) ≅ (CategoryTheory.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

• commMonTypeEquivalenceCommMonForget = CategoryTheory.Iso.refl (CommMonTypeEquivalenceCommMon.functor.comp (CategoryTheory.forget₂ CommMonCat MonCat))