∀ (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 : C),
  CategoryTheory.CategoryStruct.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
        ((CategoryTheory.NatIso.ofComponents
                (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))))
                ⋯).hom.app
          (Opposite.op (CategoryTheory.Join.left a))))
      ((CategoryTheory.NatIso.ofComponents
              (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)))
              ⋯).hom.app
        ((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
          (Opposite.op (CategoryTheory.Join.left a)))) =
    CategoryTheory.CategoryStruct.id
      ((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
        (Opposite.op (CategoryTheory.Join.left a)))