Documentation

Mathlib.CategoryTheory.Bicategory.End

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

source
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.

Instances For
    source
    instance CategoryTheory.instCategoryEndMonoidal {C : Type u_1} [CategoryTheory.Bicategory C] (X : C) :
    CategoryTheory.Category.{u_2, u_3} (CategoryTheory.EndMonoidal X)
    source
    instance CategoryTheory.instInhabitedEndMonoidal {C : Type u_1} [CategoryTheory.Bicategory C] (X : C) :
    Inhabited (CategoryTheory.EndMonoidal X)
    source
    instance CategoryTheory.instMonoidalCategoryEndMonoidalInstCategoryEndMonoidal {C : Type u_1} [CategoryTheory.Bicategory C] (X : C) :
    CategoryTheory.MonoidalCategory (CategoryTheory.EndMonoidal X)