∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {α : Type u_2} {B : C} {X Y : α → C}
  (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ (a : α), CategoryTheory.Epi (g a)]
  [CategoryTheory.EffectiveEpiFamily Y fun a => CategoryTheory.CategoryStruct.comp (g a) (f a)],
  CategoryTheory.EffectiveEpiFamily X f