Definition 2.2.2.  Let S be a pointed set. We define
(S)
by:
([S, s]) := S  (S is a set, s ∈ S)
We write “let x ∈ S” for “let x ∈ (S).”
Remarks.

This definition retrieves a representative carrier set from a pointed set (which is actually an equivalence class of pointed sets), and enables typical abuse of notation.