∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_1, u_3} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (D : Type u_4) [inst_3 : CategoryTheory.Category.{u_2, u_4} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {X Y Z : CategoryTheory.LaxBraidedFunctor C D} (f : X ⟶ Y) (g : Y ⟶ Z),
  {
      app := fun A =>
        CategoryTheory.CommMon.homMk
          (CategoryTheory.Mon.Hom.mk' ((CategoryTheory.CategoryStruct.comp f g).hom.hom.app A.X) ⋯ ⋯),
      naturality := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      { app := fun A => CategoryTheory.CommMon.homMk (CategoryTheory.Mon.Hom.mk' (f.hom.hom.app A.X) ⋯ ⋯),
        naturality := ⋯ }
      { app := fun A => CategoryTheory.CommMon.homMk (CategoryTheory.Mon.Hom.mk' (g.hom.hom.app A.X) ⋯ ⋯),
        naturality := ⋯ }