{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (section_ : Y ⟶ X) →
          autoParam (CategoryTheory.CategoryStruct.comp section_ f = CategoryTheory.CategoryStruct.id Y)
              CategoryTheory.SplitEpi.id._autoParam →
            CategoryTheory.SplitEpi f