∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {Z : C} {I : CategoryTheory.InjectiveResolution Z} {Z' : C}
  {I' : CategoryTheory.InjectiveResolution Z'} {f : Z ⟶ Z'} (φ : I.Hom I' f) {Z_1 : CochainComplex C ℕ}
  (h : I'.cocomplex ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp I.ι (CategoryTheory.CategoryStruct.comp φ.hom h) =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) (CategoryTheory.CategoryStruct.comp I'.ι h)