How should a "working mathematician" think about sets? (ZFC, category theory, urelements)

Set theory provides a foundation for mathematics in roughly the same way that Turing machines provide a foundation for computer science. A computer program written in Java or assembly language isn't actually a Turing machine, and there are lots of good reasons not to do real programming in Turing machines - real languages have all sorts of useful higher order concepts. But Turing machines are a useful foundation because everything else can be encoded by Turing machines, and because it's much easier to study Turing machines than it is to study a more complicated higher order language.

Similarly, the point isn't that every mathematical object is a set, the point is that every mathematical object can be encoded by a set. It doesn't represent higher level ideas, like the fact that mathematical objects usually have types (as one of my colleagues likes to point out, the question "is the integer 6 an abelian group" is technically a reasonable one in set theory, but not in mathematics). But it's a (relatively) simple system to study, and just about everything we want to do can be encoded in set theory.

To answer your specific questions, yes, it's still true that every mathematical object can be encoded as a set. Because sets are very flexible, there's no reason to think this will not continue to be true. There is no current field of mathematics in which urelements are essential, and because things one would do with urelements can instead be encoded with sets, there is unlikely to be such a field.

ZFC does impose some limitations on category theory, because it doesn't allow objects on the same scale of the universe of sets. (For instance the category of categories is awkward to consider within ZFC, because the objects of this category cannot be a set.) These are reflected in the discussions of "small" and "locally small" categories. These issues can be worked around in mild extensions of ZFC by using things like Grothendieck universes. (Note that this is a feature of ZFC, not of set theoretic foundations in general. Quine's New Foundations allows certain self-containing sets.)

This way of thinking can't really be burden because ZFC doesn't impose a way of thinking. The fact that things can be encoded as sets doesn't, and shouldn't, mean that we always think of them that way. It's perfectly consistent with having a set theoretic foundation to work with things like urelements, or to think about groups and categories without thinking of them as sets. (Worrying about things like self-containing categories can be a burden, but it's a necessary one given the history of paradoxical objects containing themselves.)

I prefer to think of ZFC as a proposed model of mathematics. I want to emphasize both words "proposed" and "model". For comparison, consider quantum mechanics. It can be modeled — as far as we know, perfectly — by the theory of Hilbert spaces. But the state right now of the electron in your retinal cell being excited by photon being emitted by the leftmost pixel in this word is not a vector in a Hilbert space: there is a Hilbert space $\mathcal H$ with a vector $v \in \mathcal H$ that, so far as we know, perfectly models that physical interaction, but $(v,\mathcal H)$ is only isomorphic to the physical system, it isn't itself a physical system.

So ZFC proposes not that mathematics "is" Sets, but that mathematics is "isomorphic to" Sets.

One reason to think that ZFC remains only a proposed model is that there is continued debate about the "correct" axioms for set theory. You can find, for example, recent papers by Woodin arguing that $\mathfrak c = \aleph_2$. Certainly such arguments are not "proofs" in ZFC — the value of $\mathfrak c$ is independent of ZFC (beyond that ZFC proves $\mathfrak c > \aleph_0$) — but arguments about the "actual mathematical world" (specifically, the actual world of sets).

I wonder how Asaf will interpret this answer in terms of Platonistic burdens.

There are already some excellent answers explaining in what senses ZFC can still be a foundation for most mathematics. But it also seems appropriate to mention some ways in which ZFC is insufficient as a foundation for modern mathematics. [Disclaimer: throughout this answer I will talk about "ZFC", but the remarks apply just as well to its variations including large cardinals and so on, and in some cases require variations such as removing choice or using constructive logic.]

To start with, by asking the question the way you did, as a dichotomy between sets and "urelements", you bias the answers you're likely to get. In fact, most real-world alternatives to ZFC are not simply obtained by "adding urelements" that have no members: instead they call into question the whole assumption of ZFC that there is a "membership" relation that can be meaningfully applied to any two mathematical objects. In such theories there are basic objects, sometimes still called "sets" but other times called something else like "types", and these objects have "elements"; but we cannot compare elements of two different sets/types or ask whether one set/type is an element or subset of another.

One such theory that calls its objects "sets" is Lawvere's ETCS. Those that call their objects "types" are generally called "type theory" of one sort or another; here is a blog post I wrote introducing type theory. In general, these alternative theories are inter-translatable with ZFC (or some minor variation of it), and in particular equiconsistent. Thus, any of them can serve equally well to encode most of mathematics and thereby guarantee its consistency.

However, consistency is not the only purpose of having a foundation for mathematics. There are several other purposes that could be mentioned, but one that's particularly relevant is "change of universe" or "internalization". Any sufficiently powerful formal system like ZFC, ETCS, or type theory admits more than one model; even if we assume there is one "real" model (which is itself debatable), from that starting model we can always construct lots of other models. Moreover, it so happens that many of these other models are intrinsically interesting as mathematical objects even if we accept the original model as the only "real" one. For instance, if $X$ is any topological space, the sheaves on $X$ form a model of these theories (at least if we use constructive logic).

Now if some formal system can be used as a foundation for (some fragment of) mathematics, that means that any theorem can be encoded into that formal system, and is therefore "true internally" in any model of that formal system. If this model is not the "real" one, then that "internal" truth will be different from "real" or "external" truth, but if the model is interesting then the internal truth is generally also interesting. For instance, the theory of local rings, when interpreted internally in the model of sheaves on $X$, becomes the theory of sheaves of rings on $X$ whose stalks are all local; while the theory of real numbers becomes the theory of continuous real-valued functions on $X$. In this way, using a formal system as a foundation for mathematics allows us to get much more bang for our buck: we prove one theorem, and we automatically deduce not only the "real" version of that theorem but also the "internalized" versions of that theorem in all other models of our formal system.

The reason I bring this up is that as compared with ETCS and type theory, ZFC is poorly-adapted to this sort of use. Even if our "real" model consists of ZFC-style sets with a global membership relation, most other interesting models do not come naturally with one: they generally present as categories of one sort or another, and in general there is no way to say that one object of a category is a member of another one. So it is much more straightforward to internalize ETCS or type theory into a category than to internalize ZFC.

It is possible to internalize ZFC (or related theories) into a category, such as by first internalizing ETCS or type theory and then passing across the above-mentioned translation to ZFC. However, in many cases this involves a loss of information. To construct of a model of ZFC from a model of ETCS or type theory, we explicitly build "well-founded hereditary membership trees" of some sort or other; see for instance here. The resulting model only "sees" those sets or types in the original model that can be equipped with such a structure, sometimes called the "well-founded part" of a category. In some cases this is the whole thing; in other cases it can be quite different. So if we want our internalized theorems to apply to all objects of a category, then ZFC-style theories aren't good enough.

In the case of 1-categories, we can to a certain extent fix this problem by... adding urelements! We consider the "non-well-founded" objects of our category to be "sets of urelements", thereby including them in the resulting model of ZFC+urelements (see for instance this paper). So this actually provides an answer even to your question as phrased, "do we need urelements"? The construction is still much more involved than modeling ETCS or type theory, but at least it is possible.

More radical still is the situation for higher categories, whose objects behave internally like higher groupoids (or even higher categories themselves). No ZFC-style theory is known whose basic objects behave in this way, even allowing urelements. But there is a version of type theory, called homotopy type theory, whose types do behave like higher groupoids. (The model theory of homotopy type theory is not completely developed, but indications so far are promising.) Thus, for the purpose of internalizing in higher categories, it seems that ZFC really is insufficient.

A different way to put this last point is as follows. A central concept in homotopy theory and higher category theory is that of an $\infty$-groupoid. Unsurprisingly, because sets are very flexible, the notion of $\infty$-groupoid --- or at least A notion of $\infty$-groupoid --- can be encoded using sets (for instance, as a Kan simplicial set). However, this encoding forces the thereby-encoded $\infty$-groupoids to have certain properties, such as "Whitehead's principle" (a map inducing isomorphisms on all homotopy groups is an equivalence) or "sets cover" (every $\infty$-groupoid admits a surjective map from a discrete one). But we might not necessarily want these properties to hold: for instance, when internalizing in a higher category, with $\infty$-groupoids corresponding to objects of that category, they often turn out to be false.

So I would claim, contrary to what others have said, that ZFC does impose a way of thinking: namely, an assumption that everything should be encoded using sets. It's an observed fact that essentially all mathematical concepts can be encoded somehow as sets. But it's only an article of faith that every theorem we can prove about the encoding is necessarily true about the original concept.