∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {ι : Type t} (c : ComplexShape ι)
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', v, u} C],
  CategoryTheory.Limits.HasFilteredColimitsOfSize.{w, w', max t v, max (max t u) v} (HomologicalComplex C c)