∀ (C : Type u_3) [inst : CategoryTheory.Category.{u_2, u_3} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C]
  {X Y : CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.id (CategoryTheory.LaxBraidedFunctor (CategoryTheory.Discrete PUnit.{u_1 + 1}) C)).map f)
      ((fun F => CategoryTheory.LaxBraidedFunctor.isoOfComponents (fun x => F.mapIso (CategoryTheory.eqToIso ⋯)) ⋯ ⋯ ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun F => CategoryTheory.LaxBraidedFunctor.isoOfComponents (fun x => F.mapIso (CategoryTheory.eqToIso ⋯)) ⋯ ⋯ ⋯)
          X).hom
      (((CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.laxBraidedToCommMon C).comp
            (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraided C)).map
        f)