{C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {F : CategoryTheory.Functor C D} →
              [inst_4 : F.PreservesZeroMorphisms] →
                {motive : F.PreservesHomology → Sort u} →
                  ((preservesKernels :
                        ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
                          CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F) →
                      (preservesCokernels :
                          ∀ ⦃X Y : C⦄ (f : X ⟶ Y),
                            CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F) →
                        motive ⋯) →
                    (t : F.PreservesHomology) → motive t