∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (F : CategoryTheory.Functor C A)
  (X : CategoryTheory.Limits.FormalCoproduct C),
  ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).obj X = ∐ fun i => F.obj (X.obj i)