mathlib3

863a30af - feat(category_theory/*/algebra): epi_of_epi and mono_of_mono (#15121)

feat(category_theory/*/algebra): epi_of_epi and mono_of_mono (#15121) This PR proves that a morphism whose underlying carrier part is an epi/mono, is itself an epi/mono. Migrated and generalised from #LTE.