∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type w} (c : ComplexShape ι) [c.HasNoLoop]
  [inst_2 : CategoryTheory.Limits.HasCoproductsOfShape ι C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] {X : C},
  CategoryTheory.IsSeparator X →
    CategoryTheory.IsSeparator (∐ fun i => HomologicalComplex.separatingFamily c (fun x => X) (PUnit.unit, i))