∀ {I : Type u_1} [inst : AddMonoid I] {C : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : ∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂]
  [inst_4 : ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃]
  [inst_5 : ∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] [inst_6 : DecidableEq I]
  [inst_7 : CategoryTheory.Limits.HasInitial C]
  [inst_8 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  [inst_9 :
    ∀ (X₂ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)]
  (X₁ X₂ : CategoryTheory.GradedObject I C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.associator X₁ CategoryTheory.GradedObject.Monoidal.tensorUnit X₂).hom
      (CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.CategoryStruct.id X₁)
        (CategoryTheory.GradedObject.Monoidal.leftUnitor X₂).hom) =
    CategoryTheory.GradedObject.Monoidal.tensorHom (CategoryTheory.GradedObject.Monoidal.rightUnitor X₁).hom
      (CategoryTheory.CategoryStruct.id X₂)