mathlib

0567b7fa - feat(category_theory/limits): strong epimorphisms and strong epi-mono factorizations (#2433)

feat(category_theory/limits): strong epimorphisms and strong epi-mono factorizations (#2433) This PR contains the changes I mentioned in #2374. It contains: * the definition of a lift of a commutative square * the definition of a strong epimorphism * a proof that every regular epimorphism is strong * the definition of a strong epi-mono factorization * the class `has_strong_epi_images` * the construction `has_strong_epi_images` -> `has_image_maps` * a small number of changes which should have been part of #2423