# mathlibdocumentation

category_theory.monoidal.internal.types

# Mon_ (Type u) ≌ Mon.{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.

@[protected, instance]
Equations

Converting a monoid object in Type to a bundled monoid.

Equations

Converting a bundled monoid to a monoid object in Type.

Equations

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

Equations

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

Equations
@[protected, instance]
def Mon_Type_inhabited  :
inhabited (Mon_ (Type u))
Equations
@[protected, instance]
Equations

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

Equations

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

Equations

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

Equations

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

Equations
@[protected, instance]
Equations