mathlib documentation

category_theory.monoidal.rigid.functor_category

Functors from a groupoid into a right/left rigid category form a right/left rigid category. #

(Using the pointwise monoidal structure on the functor category.)