{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasBinaryCoproducts C] →
      {A : C} → CategoryTheory.Over A → CategoryTheory.Functor (CategoryTheory.Over A) (CategoryTheory.Over A)