feat(Mathlib/CategoryTheory/EffectiveEpi/Types): Effective epi in types (#29958)

This PR characterizes effective epimorphisms in the category `Type u`, proving that a function of types is an effective epimorphism if and only if it is surjective.

The main results:

`regularEpi_iff_surjective`: A function f : `X → Y` in `Type u` is a regular epimorphism if and only if it is surjective.
`effectiveEpi_iff_surjective`: A function f : `X → Y` in `Type u` is an effective epimorphism if and only if it is surjective.

Author: yonggyuchoimath

Mathlib/CategoryTheory/Types/Basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Stephen Morgan, Kim Morrison, Johannes Hölzl
 -/
 import Mathlib.CategoryTheory.EpiMono
-import Mathlib.CategoryTheory.Functor.FullyFaithful
 import Mathlib.Data.Set.CoeSort
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.ToAdditive
@@ -358,6 +357,11 @@ instance : SplitEpiCategory (Type u) where
       { section_ := Function.surjInv <| (epi_iff_surjective f).1 hf
         id := funext <| Function.rightInverse_surjInv <| (epi_iff_surjective f).1 hf }
 
+theorem isSplitEpi_iff_surjective {X Y : Type u} (f : X ⟶ Y) :
+    IsSplitEpi f ↔ Function.Surjective f :=
+  Iff.intro (fun _ => surjective_of_epi _)
+    fun hf => (by simp only [(epi_iff_surjective f).mpr hf, isSplitEpi_of_epi])
+
 end CategoryTheory
 
 -- We prove `equivIsoIso` and then use that to sneakily construct `equivEquivIso`.