∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (braiding braiding_1 :
    (X Y : C) →
      CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X)
  (e_braiding : braiding = braiding_1)
  (braiding_naturality_right :
    ∀ (X : C) {Y Z : C} (f : Y ⟶ Z),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (braiding X Z).hom =
        CategoryTheory.CategoryStruct.comp (braiding X Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
  (braiding_naturality_left :
    ∀ {X Y : C} (f : X ⟶ Y) (Z : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (braiding Y Z).hom =
        CategoryTheory.CategoryStruct.comp (braiding X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f))
  (hexagon_forward :
    ∀ (X Y Z : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
          (CategoryTheory.CategoryStruct.comp (braiding X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
            (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (braiding X Y).hom Z)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (braiding X Z).hom)))
  (hexagon_reverse :
    ∀ (X Y Z : C),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
          (CategoryTheory.CategoryStruct.comp (braiding (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
            (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (braiding Y Z).hom)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
            (CategoryTheory.MonoidalCategoryStruct.whiskerRight (braiding X Z).hom Y))),
  { braiding := braiding, braiding_naturality_right := braiding_naturality_right,
      braiding_naturality_left := braiding_naturality_left, hexagon_forward := hexagon_forward,
      hexagon_reverse := hexagon_reverse } =
    { braiding := braiding_1, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯,
      hexagon_reverse := ⋯ }