{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {s : CategoryTheory.Limits.CokernelCofork f} →
            CategoryTheory.Limits.IsColimit s →
              {W : C} →
                (k : Y ⟶ W) →
                  CategoryTheory.CategoryStruct.comp f k = 0 →
                    { l // CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Cofork.π s) l = k }