{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        {M N : C} →
          (e : M ≅ N) →
            [inst_3 : CategoryTheory.MonObj M] →
              [inst_4 : CategoryTheory.IsCommMonObj M] →
                [inst_5 : CategoryTheory.MonObj N] →
                  [inst_6 : CategoryTheory.IsCommMonObj N] →
                    [CategoryTheory.IsMonHom e.hom] →
                      { X := M, mon := inst_3, comm := inst_4 } ≅ { X := N, mon := inst_5, comm := inst_6 }