Commit 2023-11-16 09:53 886de864
View on Github →feat(CategoryTheory): relate mathlib's notion of EffectiveEpi to more standard definitions and RegularEpi (#8426)
We prove that RegularEpi implies EffectiveEpi in full generality, and its converse under additional hypotheses.