Definition 2.5.2.  We define:
Mon:=: {[M, , e] | M is a set, :M × M → M is an operation on M, e ∈ M such that (M, , e) forms a monoid}
[M, , e] = [N, , f]  :⇔  ∃ φ:M ↔ N : [φ and eφf]  (M is a set, :M × M → M is an operation on M, e ∈ M, N is a set, :N × N → N is an operation on N, f ∈ N with suitable conditions)
We write “let M be a monoid” for “let M ∈ Mon.”
References.