Commit 2025-10-02 12:58 ca55add7
View on Github →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.