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.)

instance CategoryTheory.Monoidal.functorHasRightDual {C : Type u_1} {D : Type u_2} [CategoryTheory.Groupoid C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.RightRigidCategory D] (F : CategoryTheory.Functor C D) : CategoryTheory.HasRightDual F

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Monoidal.rightRigidFunctorCategory {C : Type u_1} {D : Type u_2} [CategoryTheory.Groupoid C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.RightRigidCategory D] : CategoryTheory.RightRigidCategory (CategoryTheory.Functor C D)

Equations

• CategoryTheory.Monoidal.rightRigidFunctorCategory = CategoryTheory.RightRigidCategory.mk

instance CategoryTheory.Monoidal.functorHasLeftDual {C : Type u_1} {D : Type u_2} [CategoryTheory.Groupoid C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.LeftRigidCategory D] (F : CategoryTheory.Functor C D) : CategoryTheory.HasLeftDual F

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Monoidal.leftRigidFunctorCategory {C : Type u_1} {D : Type u_2} [CategoryTheory.Groupoid C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.LeftRigidCategory D] : CategoryTheory.LeftRigidCategory (CategoryTheory.Functor C D)

Equations

• CategoryTheory.Monoidal.leftRigidFunctorCategory = CategoryTheory.LeftRigidCategory.mk

instance CategoryTheory.Monoidal.rigidFunctorCategory {C : Type u_1} {D : Type u_2} [CategoryTheory.Groupoid C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.RigidCategory D] : CategoryTheory.RigidCategory (CategoryTheory.Functor C D)

Equations

• CategoryTheory.Monoidal.rigidFunctorCategory = CategoryTheory.RigidCategory.mk