If D has finite (co)limits, so do the functor categories C ⥤ D.

These are boiler-plate instances, in their own file as neither import otherwise needs the other.

instance CategoryTheory.Limits.functor_category_hasFiniteLimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteLimits D] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Functor C D)

Equations

• (_ : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Functor C D)) = (_ : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Functor C D))

instance CategoryTheory.Limits.functor_category_hasFiniteColimits {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasFiniteColimits D] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Functor C D)

Equations

• (_ : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Functor C D)) = (_ : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Functor C D))