Endomorphisms of an object in a bicategory, as a monoidal category.

def CategoryTheory.EndMonoidal {C : Type u_1} [CategoryTheory.Bicategory C] (X : C) : Type u_3

The endomorphisms of an object in a bicategory can be considered as a monoidal category.

Equations

• CategoryTheory.EndMonoidal X = (X ⟶ X)

instance CategoryTheory.instCategoryEndMonoidal {C : Type u_1} [CategoryTheory.Bicategory C] (X : C) : CategoryTheory.Category.{u_2, u_3} (CategoryTheory.EndMonoidal X)

Equations

• CategoryTheory.instCategoryEndMonoidal X = inferInstance

instance CategoryTheory.instInhabitedEndMonoidal {C : Type u_1} [CategoryTheory.Bicategory C] (X : C) : Inhabited (CategoryTheory.EndMonoidal X)

Equations

• CategoryTheory.instInhabitedEndMonoidal X = { default := CategoryTheory.CategoryStruct.id X }

instance CategoryTheory.instMonoidalCategoryEndMonoidal {C : Type u_1} [CategoryTheory.Bicategory C] (X : C) : CategoryTheory.MonoidalCategory (CategoryTheory.EndMonoidal X)

Equations

• CategoryTheory.instMonoidalCategoryEndMonoidal X = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯