∀ {β : Type w} {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : α → C) (g : β → C)
  [CategoryTheory.Limits.HasCoproduct f] (e : β ≃ α) (iso : (j : β) → g j ≅ f (e j)),
  CategoryTheory.Limits.HasCoproduct g