Theorems · Definition · category theory

CategoryTheory.endofunctorMonoidalCategory

(C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MonoidalCategory (CategoryTheory.Functor C C)

The category of endofunctors of any category is a monoidal category, with tensor product given by composition of functors (and horizontal composition of natural transformations). Note: due to the fact that composition of functors in mathlib is reversed compared to the one usually found in the literature, this monoidal structure is in fact the monoidal opposite of the one usually considered in the literature.

Defined in

Mathlib.CategoryTheory.Monoidal.End

Cited by

118 results in Mathlib

Foundations

Depth 29 from the axioms, rests on 138 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Category