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