∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S S₁ : CategoryTheory.ShortComplex C} {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology] (φ : S₁ ⟶ S) [inst_3 : S₁.HasRightHomology],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.opcyclesMap φ) (S.descOpcycles k hk) =
    S₁.descOpcycles (CategoryTheory.CategoryStruct.comp φ.τ₂ k) ⋯