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.
Mathlib.CategoryTheory.Limits.Shapes.FunctorCategory
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.