E.1.2 MONOID

spec

MONOID =

sort

M

ops

n : M;
__*__ : M × M   ->   M, assoc, unit n

%% 

Alternatively, just specify the corresponding axioms:

vars

x,y,z : M

  ·  

n*x=x

  ·  

x*n=x

  ·  

(x*y)*z=x*(y*z)