{I : Type w₀} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₀} →
        {D : J → Type u₁} →
          [inst_1 : (j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] →
            CategoryTheory.Functor ((i : I) → C i)
              (CategoryTheory.Functor ((j : J) → D j) ((s : I ⊕ J) → Sum.elim C D s))