{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type v} →
      [inst_1 : CategoryTheory.SmallCategory I] →
        (F : CategoryTheory.Functor I (CategoryTheory.Functor Cᵒᵖ (Type v))) →
          {J : Type v} →
            [inst_2 : CategoryTheory.SmallCategory J] →
              (G :
                  CategoryTheory.Functor J
                    (CategoryTheory.CostructuredArrow CategoryTheory.yoneda (CategoryTheory.Limits.colimit F))) →
                {K : Type v} →
                  [inst_3 : CategoryTheory.SmallCategory K] →
                    (H : CategoryTheory.Functor K (CategoryTheory.Over (CategoryTheory.Limits.colimit F))) →
                      (G.op.comp
                              (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                                  (CategoryTheory.Limits.colimit F)).op).comp
                          (CategoryTheory.yoneda.obj (CategoryTheory.Limits.colimit H)) ≅
                        CategoryTheory.Limits.colimit
                          (H.comp
                            (CategoryTheory.yoneda.comp
                              ((CategoryTheory.Functor.whiskeringLeft Jᵒᵖ
                                    (CategoryTheory.Over (CategoryTheory.Limits.colimit F))ᵒᵖ (Type (max u v))).obj
                                (G.op.comp
                                  (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda
                                      (CategoryTheory.Limits.colimit F)).op))))