∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_3}
  {I₂ : Type u_4} {I₁₂ : Type u_5} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂) (c₁₂ : ComplexShape I₁₂)
  [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂]
  [inst_4 : ∀ (K : HomologicalComplex₂ C c₁ c₂), K.HasTotal c₁₂] (X : HomologicalComplex₂ C c₁ c₂),
  HomologicalComplex₂.total.map (CategoryTheory.CategoryStruct.id X) c₁₂ =
    CategoryTheory.CategoryStruct.id (X.total c₁₂)