{J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} →
              {motive : CategoryTheory.Limits.DiagramOfCocones F → Sort u} →
                (t : CategoryTheory.Limits.DiagramOfCocones F) →
                  ((obj : (j : J) → CategoryTheory.Limits.Cocone (F.obj j)) →
                      (map :
                          {j j' : J} →
                            (f : j ⟶ j') → obj j ⟶ (CategoryTheory.Limits.Cocones.precompose (F.map f)).obj (obj j')) →
                        (id :
                            ∀ (j : J),
                              (map (CategoryTheory.CategoryStruct.id j)).hom =
                                CategoryTheory.CategoryStruct.id (obj j).pt) →
                          (comp :
                              ∀ {j₁ j₂ j₃ : J} (f : j₁ ⟶ j₂) (g : j₂ ⟶ j₃),
                                (map (CategoryTheory.CategoryStruct.comp f g)).hom =
                                  CategoryTheory.CategoryStruct.comp (map f).hom (map g).hom) →
                            motive { obj := obj, map := map, id := id, comp := comp }) →
                    motive t