The category of type-valued sheaves is a regular epi category

This file proves that when the target category D is a regular epi category (i.e. every epimorphism is regular) and has pushouts and kernel pairs of epimorphisms, the functor category C ⥤ D is a regular epi category. This is an instance that applies directly when D is Type*.

instance CategoryTheory.Functor.instIsRegularEpiCategoryOfForallEpiHasPullbackOfHasPushouts {C : Type u_1} {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] [∀ {F G : D} (f : F ⟶ G) [Epi f], Limits.HasPullback f f] [Limits.HasPushouts D] [IsRegularEpiCategory D] : IsRegularEpiCategory (Functor C D)