{C : Type u_2} →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {P : CategoryTheory.ProjectiveResolution Y} →
          {Q : CategoryTheory.ProjectiveResolution Z} →
            (f : P.complex ⟶ Q.complex) →
              (n : ℕ) →
                (motive :
                    (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ×'
                        (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
                          f.f (n + 1) =
                            CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) f_1 +
                              CategoryTheory.CategoryStruct.comp f' (Q.complex.d (n + 2) (n + 1)) →
                      Sort u_3) →
                  (x :
                      (f_1 : P.complex.X n ⟶ Q.complex.X (n + 1)) ×'
                        (f' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) ×'
                          f.f (n + 1) =
                            CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) f_1 +
                              CategoryTheory.CategoryStruct.comp f' (Q.complex.d (n + 2) (n + 1))) →
                    ((g : P.complex.X n ⟶ Q.complex.X (n + 1)) →
                        (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) →
                          (w :
                              f.f (n + 1) =
                                CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g +
                                  CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1))) →
                            motive ⟨g, ⟨g', w⟩⟩) →
                      motive x