Monoid

$\textbf{Monoid} \; A \; \otimes \; I$

---

$\textbf{Semigroup} \; A \; \otimes$

$\textbf{Unital} \; A \; \otimes \; I$

---

pred Monoid(A: set univ, op: univ->univ->univ, I: univ) {
  Semigroup[A,op]
  Unital[A,op,I]
}