mathlib3 documentation


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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

Instances for category_theory.End_monoidal