∀ {K : Type u₂} [inst : CategoryTheory.Category.{v₂, u₂} K] [Small.{v, u₂} K] [CategoryTheory.IsFiltered K] {C : Type u}
  [inst_3 : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type v}
  [inst_4 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_5 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.forget C)]
  [CategoryTheory.Limits.PreservesColimitsOfShape K (CategoryTheory.forget C)] [CategoryTheory.Limits.HasFiniteLimits C]
  [inst_9 : CategoryTheory.Limits.HasColimitsOfShape K C] [(CategoryTheory.forget C).ReflectsIsomorphisms],
  CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Limits.colim