mathlib documentation

category_theory.bicategory.End

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

def category_theory.End_monoidal {C : Type u_1} [category_theory.bicategory C] (X : C) :
Type u_3

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

Equations
Instances for category_theory.End_monoidal