∀ (C : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X Y Z : CategoryTheory.Mon (CategoryTheory.Comon C)} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.Comon.Hom.mk' ((CategoryTheory.Comon.forget C).mapMon.map (CategoryTheory.CategoryStruct.comp f g)) ⋯
      ⋯ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Comon.Hom.mk' ((CategoryTheory.Comon.forget C).mapMon.map f) ⋯ ⋯)
      (CategoryTheory.Comon.Hom.mk' ((CategoryTheory.Comon.forget C).mapMon.map g) ⋯ ⋯)