∀ {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 : (x x_1 x_2 : CategoryTheory.Join C D) → x.Hom x_1 → x_1.Hom x_2 → Sort u_5) (_x _y : C) (_z : D)
  (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y))
  (x_1 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z))
  (h_1 :
    (_x _y _z : C) →
      (f : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
        (g : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.left _z)) →
          motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.left _z) f g)
  (h_2 :
    (_x _y : C) →
      (_z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
          (x_2 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y) (CategoryTheory.Join.right _z) x x_2)
  (h_3 :
    (_x : C) →
      (_y _z : D) →
        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y)) →
          (x_2 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) x x_2)
  (h_4 :
    (_x _y _z : D) →
      (f : (CategoryTheory.Join.right _x).Hom (CategoryTheory.Join.right _y)) →
        (g : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
          motive (CategoryTheory.Join.right _x) (CategoryTheory.Join.right _y) (CategoryTheory.Join.right _z) f g),
  (match CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.right _z, x, x_1 with
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.left _z, f, g => h_1 _x _y _z f g
    | CategoryTheory.Join.left _x, CategoryTheory.Join.left _y, CategoryTheory.Join.right _z, x, x_2 =>
      h_2 _x _y _z x x_2
    | CategoryTheory.Join.left _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, x, x_2 =>
      h_3 _x _y _z x x_2
    | CategoryTheory.Join.right _x, CategoryTheory.Join.right _y, CategoryTheory.Join.right _z, f, g =>
      h_4 _x _y _z f g) =
    h_2 _x _y _z x x_1