{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {D : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {X Y : D} →
              (i : X ⟶ Y) →
                [inst_4 : CategoryTheory.Limits.HasCokernel i] →
                  (F : CategoryTheory.Functor D C) →
                    [F.PreservesZeroMorphisms] →
                      [CategoryTheory.Mono (F.map i)] →
                        [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair i 0) F] →
                          CategoryTheory.Limits.IsLimit (F.mapCone (CategoryTheory.Limits.KernelFork.ofι i ⋯))