Reflecting the property of being preregular

We prove that given a fully faithful functor F : C ⥤ D, with Preregular D, 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 Preregular.

theorem CategoryTheory.Functor.reflects_preregular {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesEffectiveEpis] [F.ReflectsEffectiveEpis] [F.EffectivelyEnough] [Preregular D] [F.Full] [F.Faithful] : Preregular C