{C : Type u_1} →
  [inst : CategoryTheory.Category.{u_4, u_1} C] →
    {I : Type u_2} →
      {D : I → Type u_3} →
        [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] →
          {F : (i : I) → CategoryTheory.Functor C (D i)} →
            {motive : CategoryTheory.JointlyReflectIsomorphisms F → Sort u} →
              (t : CategoryTheory.JointlyReflectIsomorphisms F) →
                ((isIso :
                      ∀ {X Y : C} (f : X ⟶ Y) [∀ (i : I), CategoryTheory.IsIso ((F i).map f)], CategoryTheory.IsIso f) →
                    motive ⋯) →
                  motive t