{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (φ : S₁ ⟶ S₂) →
          (hf₁ : S₁.f = 0) →
            (c₁ : CategoryTheory.Limits.KernelFork S₁.g) →
              (hc₁ : CategoryTheory.Limits.IsLimit c₁) →
                (hf₂ : S₂.f = 0) →
                  (c₂ : CategoryTheory.Limits.KernelFork S₂.g) →
                    (hc₂ : CategoryTheory.Limits.IsLimit c₂) →
                      (f : c₁.pt ⟶ c₂.pt) →
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c₁) φ.τ₂ =
                            CategoryTheory.CategoryStruct.comp f (CategoryTheory.Limits.Fork.ι c₂) →
                          CategoryTheory.ShortComplex.RightHomologyMapData φ
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁)
                            (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂)