Set theories that do require the existence of urelements? I am looking for an axiomatic set theory that not only admits the existence of urelements/atoms (via two-sortedness or an additional unary predicate) but requires it, e.g. by an axiom like "for each set there is an equipollent set of urelements" (= "there are arbitrarily many urelements"). Any references?
 A: Your question is equivalent to asking whether the urelements, or atoms, can form a proper class. This axiom is consistent with ZFA, but usually ZFA is introduced so as to not insist on this (and indeed, not insist on any atoms at all). I believe that many (or most) of the other standard set-theories-with-urelements also allow this. 
Andreas Blass has an article here, where he investigates the connection between some theorems in homological algebra and the Axiom of Choice. In his introduction, he states: 


In Section 3, we construct a model of set theory with no nontrivial injective abelian groups. It is a permutation model in which the atoms (= urelements) form a proper class;


In contrast, sometimes it is useful to have only a set of atoms, as witnessed by Eric Hall's article, which contains the following remark.


Definitions and Conventions. The theory ZFA is a modification of ZF allowing atoms, also
    known as urelements. See Jech [4] for a precise definition. A model of ZFA may have a proper
    class of atoms; however, for this paper we redefine ZFA to include an axiom which says that
    the class of atoms is a set (always denoted by A).


A: Nominal logic is based on the Frænkel-Mostowski permutation model of set theory.  In particular Nominal logic has a freshness axiom that states ${\forall}x. {\exists}a \in \mathbb{A}. a \# x$, where $\mathbb{A}$ is the set of atoms and # is a definable relation which is a bit too complicated to put here.
For reference, see the work by Andrew Pitts and Murdoch Gabbay.  For example "A New Approach to Abstract Syntax Involving Binders".
A: In the final end I found such a theory, it's called ZFCUA (= Zermelo Frankel set theory with the axiom of choice and unlimited atoms), see Faithful Representation in Set Theory with Atoms by Harvey Friedman.
The relevant axiom is #11: "There is no set consisting of all atoms."
A consequence of this axiom is, that there definitely are atoms (since the empty set is a set) and furthermore, that there are so many, that the collection of all of them is not a set but a proper class.
A: I don't know if this is exactly what you're looking for, but it's a theorem of NFU+Choice that $|\mathcal{P}(V)| < |V|$---which has as a corollary not only that there are atoms, but that the set of atoms is equipollent with the universe.
(A somewhat more disquieting way of putting this is that there are more atoms than there are sets.)
A: In "Parts of Classes" David Lewis builds a set theory on the foundation of singletons that are all urlements. He also enlarges this set theory to include mereology, by extending the notion of ∈ so as to mean "part of" when talking of ur-elements and how they are parts of each other.
