Symmetric Monoidal Preorder

$\textbf{SymmetricMonoidalPreorder} \; X \; R \; \otimes \; I$

---

$\textbf{MonoidalPreorder} \; X \; R \; \otimes \; I$

$\textbf{Symmetric} \; X \; \otimes$

---

pred SymmetricMonoidalPreorder(X: set univ, R: univ->univ, op: univ->univ->univ, I: univ) {
  MonoidalPreorder[X,R,op,I]
  Symmetric[X,op]
}