∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  (p : (b : β) → f b ⟶ g b) [∀ (i : β), CategoryTheory.Epi (p i)],
  CategoryTheory.Epi (CategoryTheory.Limits.Sigma.map p)