{V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (P Q : CochainComplex V ℕ) →
        (zero : P.X 0 ⟶ Q.X 0) →
          (one : P.X 1 ⟶ Q.X 1) →
            CategoryTheory.CategoryStruct.comp zero (Q.d 0 1) = CategoryTheory.CategoryStruct.comp (P.d 0 1) one →
              ((n : ℕ) →
                  (p :
                      (f : P.X n ⟶ Q.X n) ×'
                        (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                          CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                            CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f') →
                    (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×'
                      CategoryTheory.CategoryStruct.comp p.snd.fst (Q.d (n + 1) (n + 2)) =
                        CategoryTheory.CategoryStruct.comp (P.d (n + 1) (n + 2)) f'') →
                (n : ℕ) →
                  (f : P.X n ⟶ Q.X n) ×'
                    (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×'
                      CategoryTheory.CategoryStruct.comp f (Q.d n (n + 1)) =
                        CategoryTheory.CategoryStruct.comp (P.d n (n + 1)) f'