∀ {C : Type u_2} {ι : Type u_3} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (i : ι), (S.X₁.sc i).HasHomology