∀ {I : Type u_1} [inst : AddCommMonoid I] {C : Type u_3} [inst_1 : CategoryTheory.Category.{u_2, u_3} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X Y : CategoryTheory.GradedObject I C)
  [inst_3 : CategoryTheory.BraidedCategory C] [inst_4 : X.HasTensor Y] [inst_5 : Y.HasTensor X],
  (CategoryTheory.CategoryStruct.comp
      (fun k =>
        CategoryTheory.GradedObject.Monoidal.tensorObjDesc fun i j hij =>
          CategoryTheory.CategoryStruct.comp (β_ (X i) (Y j)).hom
            (CategoryTheory.GradedObject.Monoidal.ιTensorObj Y X j i k ⋯))
      fun k =>
      CategoryTheory.GradedObject.Monoidal.tensorObjDesc fun i j hij =>
        CategoryTheory.CategoryStruct.comp (β_ (X j) (Y i)).inv
          (CategoryTheory.GradedObject.Monoidal.ιTensorObj X Y j i k ⋯)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.GradedObject.Monoidal.tensorObj X Y)