Sets are the only fundamental objects in the theory $\sf ZFC$. But we can use $\sf ZFC$ as a foundation for all of mathematics by encoding the various other objects we care about in terms of sets. The idea is that every statement that mathematicians care about is equivalent to some question about sets. An example of such an encoding is Kuratowski's definition of ordered pair, $(a,b) = \{\{a\},\{a,b\}\}$, which can then be used to define the cartesian product, functions, and so on.

I'm wondering how arbitrary the choice was to use sets as a foundation. Of course there are alternative foundations that don't use sets, but as far as I know all these foundations are still based on things that are quite similar to sets (for example $\sf HoTT$ uses $\infty$-groupoids, but still contains sets as a special case of these).

My suspicion is that we could instead pick almost any kind of mathematical structure to use as a foundation instead of sets and that no matter what we chose it would be possible to encode all of mathematics in terms of statements about those structures. (Of course I will add the caveat that there has to be a proper class of whichever structure we choose, up to isomorphism. I'm thinking of things like groups, topological spaces, Lie algebras, etc. Any theory about a mere set of structures will be proved consistent by $\sf ZFC$ and hence be weaker than it.)

For concreteness I'll take groups as an example of a structure very different from sets. Can every mathematical statement be encoded as a statement about groups?

Since we accept that it is possible to encode every mathematical statement as a statement about sets, it would suffice to show that set theory can be encoded in terms of groups. I've attempted a formalization of this below, but I would also be interested in any other approaches to the question.

We'll define a theory of groups, and then ask if the theory of sets (and hence everything else) can be interpreted in it. Since groups have no obvious equivalent of $\sf ZFC$'s membership relation we'll instead work in terms of groups and their homomorphisms, defining a theory of the category of groups analogous to $\sf{ETCS+R}$ for sets. The Elementary Theory of the Category of Sets, with Replacement is a theory of sets and functions which is itself biinterpretable with $\sf ZFC$.

We'll define our theory of groups by means of an interpretation in $\sf{ETCS+R}$. It will use the same language as $\sf{ETCS+R}$, but we'll interpret the objects to be groups and the morphisms to be group homomorphisms. Say the theorems of our theory are precisely the statements in this language whose translations under this interpretation are provable in $\sf{ETCS+R}$. This theory is then recursively axiomatizable by Craig's Theorem. Naturally we'll call this new theory '$\sf{ETCG+R}$'.

The theory $\sf{ETCS+R}$ is biinterpretable with $\sf ZFC$, showing that any mathematics encodable in one is encodable in the other.

Question: Is $\sf{ETCG+R}$ biinterpretable with $\sf ZFC$? If not, is $\sf ZFC$ at least interpretable in $\sf{ETCG+R}$? If not, are they at least equiconsistent?