∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X : C}
  {R : CategoryTheory.InjectiveResolution X} {X' : C} {R' : CategoryTheory.InjectiveResolution X'} {f : X ⟶ X'}
  (φ : R.Hom R' f),
  CategoryTheory.CategoryStruct.comp R.ι' φ.hom' =
    CategoryTheory.CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map f) R'.ι'