 We have alluded already to the fact that the simple typed theory of sets TST can be shown to be equivalent to an untyped theory (Mac Lane set theory, aka bounded Zermelo set theory). We briefly indicate how to do this: choose any map \(f\) in the model which is an injection with domain the set of singletons of type 0 objects and range included in type 1 (the identity on singletons of type 0 objects is an example). Identify each type 0 object \(x^0\) with the type 1 object \(f (\{x^0\})\); then introduce exactly those identifications between objects of different types which are required by extensionality: every type 0 object is identified with a type 1 object, and an easy meta-induction shows that every type \(n\) object is identified with some type \(n + 1\) object. The resulting structure will satisfy all the axioms of Zermelo set theory except Separation, and will satisfy all instances of Separation in which each quantifier is bounded in a set (this boundedness comes in because each instance of Comprehension in TST has each quantifier bounded in a type, which becomes a bounding set for that quantifier in the interpretation of Mac Lane set theory). It will satisfy Infinity and Choice if the original model of TST satisfies these axioms. The simplest map \(f\) is just the identity on singletons of type 0 objects, which will have the effect of identifying each type 0 object with its own singleton (a failure of foundation). It can be arranged for the structure to satisfy Foundation: for example, if Choice holds type 0 can be well-ordered and each element of type 0 identified with the corresponding segment in the well-ordering, so that type 0 becomes a von Neumann ordinal. (A structure of this kind will never model Replacement, as there will be a countable sequence of cardinals [the cardinalities of the types] which is definable and cofinal below the cardinality of the universe.) See Mathias 2001a for a full account.