{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (braiding :
          (X Y : C) →
            CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) →
        autoParam
            (∀ (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))
            CategoryTheory.BraidedCategory.braiding_naturality_right._autoParam →
          autoParam
              (∀ {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))
              CategoryTheory.BraidedCategory.braiding_naturality_left._autoParam →
            autoParam
                (∀ (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)))
                CategoryTheory.BraidedCategory.hexagon_forward._autoParam →
              autoParam
                  (∀ (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)))
                  CategoryTheory.BraidedCategory.hexagon_reverse._autoParam →
                autoParam
                    (∀ (X Y : C),
                      CategoryTheory.CategoryStruct.comp (braiding X Y).hom (braiding Y X).hom =
                        CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
                    CategoryTheory.SymmetricCategory.symmetry._autoParam →
                  CategoryTheory.SymmetricCategory C