Documentation

Mathlib.CategoryTheory.Limits.FunctorCategory.Filtered

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.