Definition 2.2.1. We define:

PtSet :=: {[*S*, *s*] | *S* is a set, *s* ∈ *S*}

We write “let S be a pointed set” for “let S ∈ PtSet.”

Remarks.

Strictly speaking, the elements of this set are not pointed sets but isomorphism classes of pointed sets, which are similar to cardinal numbers (see `$../../Essentials/Numbers/Cardinal/"Cardinal numbers"`

). Due to the rules of HLM, it is not even possible to define pointed sets (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.