∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_1, u_3} C] {D : Type u_4}
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D]
  (motive : CategoryTheory.Join C D → CategoryTheory.Join C D → Sort u_5) (a : C) (a_1 : D)
  (h_1 : (x y : C) → motive (CategoryTheory.Join.left x) (CategoryTheory.Join.left y))
  (h_2 : (x y : D) → motive (CategoryTheory.Join.right x) (CategoryTheory.Join.right y))
  (h_3 : (a : C) → (a_2 : D) → motive (CategoryTheory.Join.left a) (CategoryTheory.Join.right a_2))
  (h_4 : (a : D) → (a_2 : C) → motive (CategoryTheory.Join.right a) (CategoryTheory.Join.left a_2)),
  (match CategoryTheory.Join.left a, CategoryTheory.Join.right a_1 with
    | CategoryTheory.Join.left x, CategoryTheory.Join.left y => h_1 x y
    | CategoryTheory.Join.right x, CategoryTheory.Join.right y => h_2 x y
    | CategoryTheory.Join.left a, CategoryTheory.Join.right a_2 => h_3 a a_2
    | CategoryTheory.Join.right a, CategoryTheory.Join.left a_2 => h_4 a a_2) =
    h_3 a a_1