∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X : C}
  (β :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X)
  (monoidal :
    autoParam
      (∀ (U U' : C),
        (β (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam)
  (naturality :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β U').hom =
          CategoryTheory.CategoryStruct.comp (β U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam)
  (β_1 :
    (U : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X U ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj U X)
  (monoidal_1 :
    autoParam
      (∀ (U U' : C),
        (β_1 (CategoryTheory.MonoidalCategoryStruct.tensorObj U U')).hom =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X U U').inv
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_1 U).hom U')
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator U X U').hom
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft U (β_1 U').hom)
                  (CategoryTheory.MonoidalCategoryStruct.associator U U' X).inv))))
      CategoryTheory.HalfBraiding.monoidal._autoParam)
  (naturality_1 :
    autoParam
      (∀ {U U' : C} (f : U ⟶ U'),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_1 U').hom =
          CategoryTheory.CategoryStruct.comp (β_1 U).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X))
      CategoryTheory.HalfBraiding.naturality._autoParam),
  ({ β := β, monoidal := monoidal, naturality := naturality } =
      { β := β_1, monoidal := monoidal_1, naturality := naturality_1 }) =
    (β = β_1)