mathlib3

c2b7d237 - chore(category_theory/limits): separate regular and normal monos (#5149)

chore(category_theory/limits): separate regular and normal monos (#5149) This separates the file `regular_mono` into `regular_mono` and `normal_mono`: mostly this simplifies the import graph, but also this has the advantage that to use things about kernel pairs it's no longer necessary to import things about zero objects (I kept changing equalizers and using the changes in a file about monads which imported kernel pairs, and it was very slow because of zero objects)