∀ (C : Type u_4) (D : Type u_3) [inst : CategoryTheory.Category.{u_2, u_4} C]
  [inst_1 : CategoryTheory.Category.{u_1, u_3} D] {X Y : CategoryTheory.Join Dᵒᵖ Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight C D).op (CategoryTheory.Join.inclLeft C D).op
                {
                  app := fun x =>
                    (CategoryTheory.Join.edge (Opposite.unop ((CategoryTheory.Prod.snd Dᵒᵖ Cᵒᵖ).obj x))
                        (Opposite.unop ((CategoryTheory.Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                  naturality := ⋯ }).comp
            (CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).rightOp
                (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                {
                  app := fun x =>
                    (CategoryTheory.Join.edge (Opposite.op ((CategoryTheory.Prod.snd C D).obj x))
                        (Opposite.op ((CategoryTheory.Prod.fst C D).obj x))).op,
                  naturality := ⋯ }).leftOp).map
        f)
      ((fun x =>
            match x with
            | CategoryTheory.Join.left a =>
              CategoryTheory.Iso.refl
                (((CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight C D).op
                          (CategoryTheory.Join.inclLeft C D).op
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.unop ((CategoryTheory.Prod.snd Dᵒᵖ Cᵒᵖ).obj x))
                                  (Opposite.unop ((CategoryTheory.Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                            naturality := ⋯ }).comp
                      (CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).rightOp
                          (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.op ((CategoryTheory.Prod.snd C D).obj x))
                                  (Opposite.op ((CategoryTheory.Prod.fst C D).obj x))).op,
                            naturality := ⋯ }).leftOp).obj
                  (CategoryTheory.Join.left a))
            | CategoryTheory.Join.right a =>
              CategoryTheory.Iso.refl
                (((CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight C D).op
                          (CategoryTheory.Join.inclLeft C D).op
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.unop ((CategoryTheory.Prod.snd Dᵒᵖ Cᵒᵖ).obj x))
                                  (Opposite.unop ((CategoryTheory.Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                            naturality := ⋯ }).comp
                      (CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).rightOp
                          (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.op ((CategoryTheory.Prod.snd C D).obj x))
                                  (Opposite.op ((CategoryTheory.Prod.fst C D).obj x))).op,
                            naturality := ⋯ }).leftOp).obj
                  (CategoryTheory.Join.right a)))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            match x with
            | CategoryTheory.Join.left a =>
              CategoryTheory.Iso.refl
                (((CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight C D).op
                          (CategoryTheory.Join.inclLeft C D).op
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.unop ((CategoryTheory.Prod.snd Dᵒᵖ Cᵒᵖ).obj x))
                                  (Opposite.unop ((CategoryTheory.Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                            naturality := ⋯ }).comp
                      (CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).rightOp
                          (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.op ((CategoryTheory.Prod.snd C D).obj x))
                                  (Opposite.op ((CategoryTheory.Prod.fst C D).obj x))).op,
                            naturality := ⋯ }).leftOp).obj
                  (CategoryTheory.Join.left a))
            | CategoryTheory.Join.right a =>
              CategoryTheory.Iso.refl
                (((CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight C D).op
                          (CategoryTheory.Join.inclLeft C D).op
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.unop ((CategoryTheory.Prod.snd Dᵒᵖ Cᵒᵖ).obj x))
                                  (Opposite.unop ((CategoryTheory.Prod.fst Dᵒᵖ Cᵒᵖ).obj x))).op,
                            naturality := ⋯ }).comp
                      (CategoryTheory.Join.mkFunctor (CategoryTheory.Join.inclRight Dᵒᵖ Cᵒᵖ).rightOp
                          (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).rightOp
                          {
                            app := fun x =>
                              (CategoryTheory.Join.edge (Opposite.op ((CategoryTheory.Prod.snd C D).obj x))
                                  (Opposite.op ((CategoryTheory.Prod.fst C D).obj x))).op,
                            naturality := ⋯ }).leftOp).obj
                  (CategoryTheory.Join.right a)))
          X).hom
      ((CategoryTheory.Functor.id (CategoryTheory.Join Dᵒᵖ Cᵒᵖ)).map f)