What is "structure" and is it equivalent to its encoding? 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?
 A: 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:


*

*$F$ is full: for every morphism $g \in \mathcal{D}(FA,FB)$ there is $f \in \mathcal{C}(A,B)$ with $Ff=g$.

*$F$ is faithful: if $f,f' \in \mathcal{C}(A,B)$ with $Ff=Ff'$, then $f=f'$.

*$F$ is essentially surjective: every object of $\mathcal{D}$ is isomorphic to one in the image.


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 $F$ is not full, then there is some $g \in \mathcal{D}(FA,FB)$ which isn't in the image. Philosphically, we can imagine this as saying that there is some structure in $\mathcal{C}$ that prevents $g$ from being a morphism there, because $g$ fails to preserve it. Non-full functors forget structure.

*If $F$ is not faithful, then there are nonequal $f,f' \in \mathcal{C}(A,B)$ with $Ff=Ff'$. We can view this as saying that there was something in $A$ that they acted differently on and let us tell them apart, but that stuff isn't present in $FA$. Non-faithful functors forget material stuff.

*If $F$ is not essentially surjective, then there is $D \in ob(\mathcal{D})$ that is not isomorphic to an object in the image. This is a property that lets us distinguish between objects that could have been in the image and those that couldn't. Non-essentially-surjective functors forget properties.


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.
