{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hg₁ : S₁.g = 0) →
            (c₁ : CategoryTheory.Limits.CokernelCofork S₁.f) →
              (hc₁ : CategoryTheory.Limits.IsColimit c₁) →
                (hg₂ : S₂.g = 0) →
                  (c₂ : CategoryTheory.Limits.CokernelCofork S₂.f) →
                    (hc₂ : CategoryTheory.Limits.IsColimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp φ.τ₂ (CategoryTheory.Limits.Cofork.π c₂) =
                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π c₁) f →
                          CategoryTheory.ShortComplex.HomologyMapData φ
                            (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.HomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂)