∀ {p q n : ℕ}
  (x :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj (SimplexCategory.mk p))
          (SSet.stdSimplex.obj (SimplexCategory.mk q))).obj
      (Opposite.op (SimplexCategory.mk n))),
  (SSet.stdSimplex.objEquiv.symm
        (SimplexCategory.Hom.mk
          (OrderHom.fst.comp
            (match x with
            | (x, y) =>
              (SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv x)).prod
                (SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv y))))),
      SSet.stdSimplex.objEquiv.symm
        (SimplexCategory.Hom.mk
          (OrderHom.snd.comp
            (match x with
            | (x, y) =>
              (SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv x)).prod
                (SimplexCategory.Hom.toOrderHom (SSet.stdSimplex.objEquiv y)))))) =
    x