∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} [inst_2 : S.HasHomology] (k : A ⟶ S.opcycles)
  (hk : CategoryTheory.CategoryStruct.comp k S.fromOpcycles = 0),
  CategoryTheory.CategoryStruct.comp (S.liftHomology k hk) S.homologyι = k