One major difference between types and sets (certainly between type theory and set theory) is that set membership is a proposition, e.g. all of the following are perfectly reasonable expressions, which ask whether or not a value exists in a set:
po ∈ point // Valid statement, which happens to be true
po ∈ my_point // Valid statement, which happens to be false
my_po ∈ point // Valid statement, which happens to be false
my_po ∈ my_point // Valid statement, which happens to be true
However, type membership is not a question; it's part of a definition. We may choose to add "annotations" to some expressions, but they only act as sanity checks; they are logically/computationally irrelevant:
po : point // Valid expression, since the annotation passes the type checker; equivalent to `po`
po : my_point // Invalid expression, since the annotation doesn't pass the type checker
my_po : point // Invalid expression, since the annotation doesn't pass the type checker
my_po : my_point // Valid expression, since the annotation passes the type checker; equivalent to `my_po`
Another way of stating this is to say that sets are “extensional” and types are “intensional,” which means that a set is defined by imposing conditions (constraints) on the membership or by simply listing the objects, while a type is defined by describing its “meaning,” e.g. by specifying operations on objects.
