[sagebird]

If urelements may be distinct from each other, or the same, it seems like you could place the universe under a type and name it urelement, without creating a new axiom -- Except for, a urelement defined in this way could never be equal to the empty set - hence the new axiom? Am I understanding this correctly?

[randallholmes]

I don't understand what you mean here.