Commit 2020-12-01 23:23 c2b7d237

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)