Definition 2.6.2.  We define:
Grp:=: {[G, , e, i] | G is a set, :G × G → G is an operation on G, e ∈ G, i:G → G is a function such that (G, , e, i) forms a group}
[G, , e, i] = [H, , f, j]  :⇔  ∃ φ:G ↔ H : [φ and eφf and iφj]  (G is a set, :G × G → G is an operation on G, e ∈ G, i:G → G is a function, H is a set, :H × H → H is an operation on H, f ∈ H, j:H → H is a function with suitable conditions)
We write “let G be a group” for “let G ∈ Grp.”
References.