∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] (D : Type u_4)
  [inst_1 : CategoryTheory.Category.{u_3, u_4} D]
  [inst_2 : ∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] (c : C) (d : D)
  (F : CategoryTheory.Functor C D) (f : d ⟶ ((CategoryTheory.evaluation C D).obj c).obj F) ⦃X Y : C⦄ (f_1 : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (((CategoryTheory.evaluationLeftAdjoint D c).obj d).map f_1)
      (CategoryTheory.Limits.Sigma.desc fun h => CategoryTheory.CategoryStruct.comp f (F.map h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.Sigma.desc fun h => CategoryTheory.CategoryStruct.comp f (F.map h)) (F.map f_1)