Preserving and reflecting effective epis on extensive categories

We prove that a functor between FinitaryPreExtensive categories preserves (resp. reflects) finite effective epi families if it preserves (resp. reflects) effective epis.

theorem CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily {C : Type u_1} [Category.{v_1, u_1} C] [FinitaryPreExtensive C] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) : EffectiveEpi (Limits.Sigma.desc π) ↔ EffectiveEpiFamily X π

instance CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis {C : Type u_1} [Category.{v_1, u_1} C] [FinitaryPreExtensive C] {D : Type u_2} [Category.{v_2, u_2} D] [FinitaryPreExtensive D] (F : Functor C D) [Limits.PreservesFiniteCoproducts F] [F.ReflectsEffectiveEpis] : F.ReflectsFiniteEffectiveEpiFamilies

instance CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis {C : Type u_1} [Category.{v_1, u_1} C] [FinitaryPreExtensive C] {D : Type u_2} [Category.{v_2, u_2} D] [FinitaryPreExtensive D] (F : Functor C D) [Limits.PreservesFiniteCoproducts F] [F.PreservesEffectiveEpis] : F.PreservesFiniteEffectiveEpiFamilies