Definition 2.3.1. We define:

Mag :=: {[*M*, ∗] | *M* is a set, ∗ : *M* × *M* → *M* is an operation on *M*}

[*M*, ∗] = [*N*, ⋆] :⇔ ∃ *φ* : *M* ↔ *N* : ∗ ≃^{φ} ⋆ (*M* is a set, ∗ : *M* × *M* → *M* is an operation on *M*, *N* is a set, ⋆ : *N* × *N* → *N* is an operation on *N*)

We write “let M be a magma” for “let M ∈ Mag.”

Remarks.

Strictly speaking, the elements of this set are not magmas but isomorphism classes of magmas. Due to the rules of HLM, it is not even possible to define magmas (or other structures) in a way that would distinguish two isomorphic structures. In particular, the requirement to specify an equality definition, together with the way two arbitrary sets are treated as separate types, make sure that in the most general case, equality is in fact the same as isomorphism. (It is possible to identify more structures, but not fewer.)

References.