∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Limits.FormalCoproduct C} (f g : X ⟶ Y),
  f = g ↔ ∃ (h₁ : f.f = g.f), ∀ (i : X.I), CategoryTheory.CategoryStruct.comp (f.φ i) (CategoryTheory.eqToHom ⋯) = g.φ i