∀ (X Y Z : SSet.Truncated 2)
  (x : X.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂._proof_1 }))
  (y₀ y₁ : Y.obj (Opposite.op { obj := SimplexCategory.mk 0, property := SSet.OneTruncation₂._proof_1 }))
  (e : SSet.Truncated.Edge y₀ y₁),
  CategoryTheory.CategoryStruct.comp
      (((CategoryTheory.Functor.curry₃.obj
                ((CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory
                        Z.HomotopyCategory).inverse.comp
                  (((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod
                        (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
                    ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse
                          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp
                      (SSet.Truncated.mapHomotopyCategory
                        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom))))).obj
            (SSet.Truncated.HomotopyCategory.mk x)).map
        (SSet.Truncated.HomotopyCategory.homMk e))
      ((fun y =>
            SSet.Truncated.HomotopyCategory.mkNatIso
              (fun z =>
                CategoryTheory.Iso.refl
                  ((((CategoryTheory.Functor.curry₃.obj
                                ((CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                        Z.HomotopyCategory).inverse.comp
                                  (((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod
                                        (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
                                    ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse
                                          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp
                                      (SSet.Truncated.mapHomotopyCategory
                                        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom))))).obj
                            (SSet.Truncated.HomotopyCategory.mk x)).obj
                        (SSet.Truncated.HomotopyCategory.mk y)).obj
                    (SSet.Truncated.HomotopyCategory.mk z)))
              ⋯)
          y₁).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun y =>
            SSet.Truncated.HomotopyCategory.mkNatIso
              (fun z =>
                CategoryTheory.Iso.refl
                  ((((CategoryTheory.Functor.curry₃.obj
                                ((CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                        Z.HomotopyCategory).inverse.comp
                                  (((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod
                                        (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
                                    ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse
                                          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).comp
                                      (SSet.Truncated.mapHomotopyCategory
                                        (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom))))).obj
                            (SSet.Truncated.HomotopyCategory.mk x)).obj
                        (SSet.Truncated.HomotopyCategory.mk y)).obj
                    (SSet.Truncated.HomotopyCategory.mk z)))
              ⋯)
          y₀).hom
      (((CategoryTheory.Functor.curry₃.obj
                (((CategoryTheory.Functor.id X.HomotopyCategory).prod
                      (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse Y Z)).comp
                  (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))).obj
            (SSet.Truncated.HomotopyCategory.mk x)).map
        (SSet.Truncated.HomotopyCategory.homMk e))