∀ {T : Type u_5} [inst : CategoryTheory.Category.{u_4, u_5} T] {V : Type u_3}
  [inst_1 : CategoryTheory.Category.{u_2, u_3} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {ι : Type u_1}
  {c : ComplexShape ι} (C : HomologicalComplex (CategoryTheory.Functor T V) c) {X Y : T} (h : X ⟶ Y) (x x_1 : ι),
  c.Rel x x_1 →
    CategoryTheory.CategoryStruct.comp ((C.X x).map h) ((C.d x x_1).app Y) =
      CategoryTheory.CategoryStruct.comp ((C.d x x_1).app X) ((C.X x_1).map h)