Simple typed set theory with atoms ($\mathrm{TSTU}$)

Objects have sorts $0,1,\dots$, with membership allowed only from sort $i$ to sort $i+1$. A set predicate distinguishes sets from atoms; atoms have no members, extensionality applies to sets, and every well-typed formula defines a set in the next sort by comprehension. First-order models may have only a specified collection of subsets, as in Henkin semantics. For a full finite-type model, take $D_i=V_{r_i}$ at widely separated increasing ranks, represent sets at level $i+1$ by $\mathcal{P}(D_i)\subseteq D_{i+1}$, and treat the remaining objects as atoms under typed membership.