{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'} →
                  {motive : I.Hom I' f → Sort u_1} →
                    ((hom : I.cocomplex ⟶ I'.cocomplex) →
                        (ι_f_zero_comp_hom_f_zero :
                            CategoryTheory.CategoryStruct.comp (I.ι.f 0) (hom.f 0) =
                              CategoryTheory.CategoryStruct.comp (((CochainComplex.single₀ C).map f).f 0) (I'.ι.f 0)) →
                          motive { hom := hom, ι_f_zero_comp_hom_f_zero := ι_f_zero_comp_hom_f_zero }) →
                      (t : I.Hom I' f) → motive t