Extensional cumulative universe over Quine atoms

Start with distinct formal atoms $q\in A$ with membership extensions $\{q\}$. Recursively adjoin a unique representative $S(X)$ of every subset $X$ of a previous stage, except that $S(\{q\})=q$ uses the atom already present. Define membership by these extensions. Each set-sized collection of objects has bounded construction rank, so it has a representative at a later stage. This gives full extensionality, unlike adjoining an ordinary singleton distinct from a Quine atom. Definable subsets and ranges, unions and power sets are set-sized collections in the ambient model and hence have representatives. The pure finite hierarchy supplies infinity. Every permutation of the atoms extends recursively; hereditary finite support restriction gives the hereditarily finite-supported Quine-atom model, whose two-element atom subsets have no choice function.