Documentation

Mathlib.CategoryTheory.Bicategory.End

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

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

Equations
Instances For