I often come across a description of sets, as objects of "zero structure". I always intuitively understood Set Theory as a theory of size, meaning that the only information we get on it's objects of study (sets) is their size (up to isomorphism of course). On the other hand, Category Theory is thought of a theory that describes structure, by way of arrows between objects, and the same can be said of type theories. I always assumed it had something to do with the functoriality of those theories, as the "structure" could a lot of the times be non-extensional (eg. an arrow in a category can be a function or something else, but it need not be described inside this category).
Are those impressions correct? If they are, is there something like a formal theory of structure in mathematical theories and a way to quantize it? And finally is it useful to think in this way as a mathematician (as opposed to metamathematician)?
The second part of my question concerns representation/encoding of mathematics in formal theories. In what way can we say that (as in the Gödel encoding of arithmetic, or as we say that ZFC is a foundation for mathematics) that mathematics is "built upon" a certain formal theory, and does this contain anything more that an encoding of a lot of math into a set of symbols?
Category Theory provides one interesting way to understand "structure" (despite being non-extensional as you said) as described here.
Given a functor between two categories, $F: \mathcal{C} \rightarrow \mathcal{D}$, we know that one way of showing that $F$ is an equivalence (and that $\mathcal{C}$ and $\mathcal{D}$ are effectively the same in terms of the structure they describe) is if:
Given that the combination of these three conditions ensures that $\mathcal{C}$ and $\mathcal{D}$ are essentially the same, it is interesting to consider what happens if each one fails:
If you try natural examples, you see that they generally support this analogy (e.g. underlying set functors are generally faithful because they keep all the stuff in the underlying set, but not full because they forget the structure on that set; given category of mathematical structures and some property they may have, the inclusion of the subcategory of objects with that property is full and faithful but not an equivalence unless every object has that property), so it becomes natural to treat these as the categorical definition of structure, properties and stuff.