∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {I₁ : Type u_2} {I₂ : Type u_3} (c₁ : ComplexShape I₁) (c₂ : ComplexShape I₂),
  (HomologicalComplex₂.flipEquivalence C c₁ c₂).counitIso = HomologicalComplex₂.flipEquivalenceCounitIso C c₁ c₂