{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 x_1 x_2 : CategoryTheory.Join C D) →
            (x_3 : x.Hom x_1) →
              (x_4 : x_1.Hom x_2) →
                ((_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) →
                  ((_x _y : C) →
                      (_z : D) →
                        (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.left _y)) →
                          (x_5 : (CategoryTheory.Join.left _y).Hom (CategoryTheory.Join.right _z)) →
                            motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.left _y)
                              (CategoryTheory.Join.right _z) x x_5) →
                    ((_x : C) →
                        (_y _z : D) →
                          (x : (CategoryTheory.Join.left _x).Hom (CategoryTheory.Join.right _y)) →
                            (x_5 : (CategoryTheory.Join.right _y).Hom (CategoryTheory.Join.right _z)) →
                              motive (CategoryTheory.Join.left _x) (CategoryTheory.Join.right _y)
                                (CategoryTheory.Join.right _z) x x_5) →
                      ((_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) →
                        motive x x_1 x_2 x_3 x_4