mathlib

093c5036 - feat(category_theory/strong_epi): various results about strong_epi (#16182)

feat(category_theory/strong_epi): various results about strong_epi (#16182) In order to prepare for the proof of the existence of strong epi mono factorisations in `simplex_category` (which shall be used for the Dold-Kan correspondence), various results are obtained, mostly about strong epimorphisms (and strong monomorphisms). If two arrows are isomorphic, then one is a strong epi iff the other is. An equivalence of categories preserves and reflects strong epimorphisms.