{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          {motive : CategoryTheory.InjectiveResolution Z → Sort u_1} →
            (t : CategoryTheory.InjectiveResolution Z) →
              ((cocomplex : CochainComplex C ℕ) →
                  (injective : ∀ (n : ℕ), CategoryTheory.Injective (cocomplex.X n)) →
                    [hasHomology : ∀ (i : ℕ), HomologicalComplex.HasHomology cocomplex i] →
                      (ι : (CochainComplex.single₀ C).obj Z ⟶ cocomplex) →
                        (quasiIso : QuasiIso ι) →
                          motive
                            { cocomplex := cocomplex, injective := injective, hasHomology := hasHomology, ι := ι,
                              quasiIso := quasiIso }) →
                motive t