Commit 2024-04-05 23:45 add80962

feat(CategoryTheory): reflecting the property of being precoherent and preregular (#11502) We prove that given a fully faitful functor F : C ⥤ D which preserves and reflects finite effective epimorphic families, such that for every object X of D there exists an object W of C with an effective epi π : F.obj W ⟶ X, the category C is Precoherent whenever D is. We prove the corresponding result for Preregular, but then it is enought that F preserves and reflects effective epis.