∀ (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] (c : C)
  (x : CategoryTheory.StructuredArrow (CategoryTheory.Join.left c) (CategoryTheory.Join.inclRight C D)),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id
              (CategoryTheory.StructuredArrow (CategoryTheory.Join.left c) (CategoryTheory.Join.inclRight C D))).obj
          x).hom
      ((CategoryTheory.Join.inclRight C D).map
        (CategoryTheory.Iso.refl
            ((CategoryTheory.Functor.id
                    (CategoryTheory.StructuredArrow (CategoryTheory.Join.left c)
                      (CategoryTheory.Join.inclRight C D))).obj
                x).right).hom) =
    (((CategoryTheory.StructuredArrow.proj (CategoryTheory.Join.left c) (CategoryTheory.Join.inclRight C D)).comp
            { obj := fun d => CategoryTheory.StructuredArrow.mk (CategoryTheory.Join.edge c d),
              map := fun {X Y} f => CategoryTheory.StructuredArrow.homMk f ⋯, map_id := ⋯, map_comp := ⋯ }).obj
        x).hom