Sets are the only fundamental objects in $\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. For example Kuratowski's definition of ordered pair, $(a,b) = \{\{a\},\{a,b\}\}$.

I'm wondering if it's necessary to use *sets* for this process, of if all of mathematics could also be encoded in terms of any kind of structure. For example, could mathematics instead be encoded in terms of groups? I've attempted to formalise this below, but I'd 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][1] 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][2]. 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?


  [1]: https://ncatlab.org/nlab/show/ETCS
  [2]: https://en.wikipedia.org/wiki/Craig%27s_theorem