∀ (C : Type u_3) (D : Type u_4) [inst : CategoryTheory.Category.{u_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{u_2, u_4} D] (a a_1 : D)
  (x : Opposite.op (CategoryTheory.Join.right a) ⟶ Opposite.op (CategoryTheory.Join.right a_1)),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.id (CategoryTheory.Join C D)ᵒᵖ).map x)
      ((fun x =>
            match x with
            | Opposite.op (CategoryTheory.Join.left a) =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.Join C D)ᵒᵖ).obj (Opposite.op (CategoryTheory.Join.left a)))
            | Opposite.op (CategoryTheory.Join.right a) =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.Join C D)ᵒᵖ).obj
                  (Opposite.op (CategoryTheory.Join.right a))))
          (Opposite.op (CategoryTheory.Join.right a_1))).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x =>
            match x with
            | Opposite.op (CategoryTheory.Join.left a) =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.Join C D)ᵒᵖ).obj (Opposite.op (CategoryTheory.Join.left a)))
            | Opposite.op (CategoryTheory.Join.right a) =>
              CategoryTheory.Iso.refl
                ((CategoryTheory.Functor.id (CategoryTheory.Join C D)ᵒᵖ).obj
                  (Opposite.op (CategoryTheory.Join.right a))))
          (Opposite.op (CategoryTheory.Join.right a))).hom
      (((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.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 := ⋯ })).map
        x)