Functor categories have filtered colimits 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.Filtered
.
These declarations cannot be in the file Mathlib.CategoryTheory.Limits.FunctorCategory
because
that file shouldn't import Mathlib.CategoryTheory.Limits.Filtered
.