∀ {J : Type u_2} {K : Type u_6} [inst : CategoryTheory.Category.{u_1, u_2} J]
  [inst_1 : CategoryTheory.Category.{u_5, u_6} K] {C : Type u_4} [inst_2 : CategoryTheory.Category.{u_3, u_4} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} {D : CategoryTheory.Limits.DiagramOfCocones F}
  (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j))
  (s : CategoryTheory.Limits.Cocone (CategoryTheory.Functor.uncurry.obj F)) {j j' : J} (f : j ⟶ j'),
  CategoryTheory.CategoryStruct.comp (D.coconePoints.map f)
      ((Q j').desc
        ((CategoryTheory.Limits.Cocones.precompose
              (CategoryTheory.NatIso.ofComponents
                  (fun x =>
                    CategoryTheory.Iso.refl
                      (((CategoryTheory.Prod.sectR j' K).comp (CategoryTheory.Functor.uncurry.obj F)).obj x))
                  ⋯).inv).obj
          (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Prod.sectR j' K) s))) =
    CategoryTheory.CategoryStruct.comp
      ((Q j).desc
        ((CategoryTheory.Limits.Cocones.precompose
              (CategoryTheory.NatIso.ofComponents
                  (fun x =>
                    CategoryTheory.Iso.refl
                      (((CategoryTheory.Prod.sectR j K).comp (CategoryTheory.Functor.uncurry.obj F)).obj x))
                  ⋯).inv).obj
          (CategoryTheory.Limits.Cocone.whisker (CategoryTheory.Prod.sectR j K) s)))
      (((CategoryTheory.Functor.const J).obj s.pt).map f)