(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.