Functor categories have finite limits when the target category does

These declarations cannot be in the file Mathlib.CategoryTheory.Limits.FunctorCategory because that file shouldn't import Mathlib.CategoryTheory.Limits.Shapes.FiniteProducts.

instance CategoryTheory.Limits.instHasFiniteLimitsFunctor {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {K : Type u_2} [CategoryTheory.Category.{u_4, u_2} K] [CategoryTheory.Limits.HasFiniteLimits C] : CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Functor K C)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.instHasFiniteProductsFunctor {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {K : Type u_2} [CategoryTheory.Category.{u_4, u_2} K] [CategoryTheory.Limits.HasFiniteProducts C] : CategoryTheory.Limits.HasFiniteProducts (CategoryTheory.Functor K C)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.instHasFiniteColimitsFunctor {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {K : Type u_2} [CategoryTheory.Category.{u_4, u_2} K] [CategoryTheory.Limits.HasFiniteColimits C] : CategoryTheory.Limits.HasFiniteColimits (CategoryTheory.Functor K C)

Equations

• ⋯ = ⋯

instance CategoryTheory.Limits.instHasFiniteCoproductsFunctor {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {K : Type u_2} [CategoryTheory.Category.{u_4, u_2} K] [CategoryTheory.Limits.HasFiniteCoproducts C] : CategoryTheory.Limits.HasFiniteCoproducts (CategoryTheory.Functor K C)

Equations

• ⋯ = ⋯