{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          (self : CategoryTheory.Abelian.AbelianStruct f) →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ self.imageπ ⋯)