Yeah, whatever, maybe some other stuff too. I should have written `epsilon N s.t. N is a minimal set that satisfies Peano's axioms`. The point is that it is not true that set theory implies some encoding. When Hilbert's epsilon is used, there is no encoding in any meaningful sense.

The main difference between type theories and set theories is that type theories have particular syntactic discipline. Everything else is or can be a feature of set theories, too.