∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} {K L : HomologicalComplex C c}
  [inst_2 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)] {A : C} {i : ι}
  {f g : (K ⊞ L).X i ⟶ A},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) f =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inl.f i) g →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.inr.f i) g →
      f = g