Return to Answer

(Thanks to Martin Brandenbourgh for pointing out the mistake in an earlier version)

An easy calculation shows that the generators and the units (Edit: that's were the mistake was) are the only elements such that $\mu(y)=y^L*y^R$ and hence that any cogroup morphism comes from a partial function between sets: each generator is sent either to a generator or to the unit.

As pointed out by Martin Brandenbourgh in his answer - once we have the category of set and partial maps, (or equivalently the category of pointed sets) one can easily characterize the category of sets and map in purely categorical language: this is the (non-full) subcategory containing all objects and whose maps are the $f:X \to Y$ such that the square obtained by adding the maps $0 \to X$ and $0\to Y$ (where $0$ is the initial object) is a pullback square.

So let's call this the category of "cogroup objects and total maps between them" (were by total, I mean the map that satisfies this pullback condition)

(Thanks to Martin Brandenburg for pointing out the mistake in an earlier version)

An easy calculation shows that the generators and the units (Edit: that's where the mistake was) are the only elements such that $\mu(y)=y^L*y^R$ and hence that any cogroup morphism comes from a partial function between sets: each generator is sent either to a generator or to the unit.

As pointed out by Martin Brandenburg in his answer - once we have the category of sets and partial maps, (or equivalently the category of pointed sets) one can easily characterize the category of sets and map in purely categorical language: this is the (non-full) subcategory containing all objects and whose maps are the $f:X \to Y$ such that the square obtained by adding the maps $0 \to X$ and $0\to Y$ (where $0$ is the initial object) is a pullback square.

So let's call this the category of "cogroup objects and total maps between them" (where by total, I mean the map that satisfies this pullback condition).

Theorem: The category of co-group objects in the category of groups is equivalent to the category of sets.

An easy calculation shows that the generators are the only elements such that $\mu(y)=y^L*y^R$ and hence that any cogroup morphism comes from a function between sets. So the only co-group morphisms are the ones sending generators to generators.

And with a bit more work, as nicely explained on this other MO answer, one can check that any cogroup object is of this form.

Now, as all this is a theorem of $\sf{ETCS}$, it is a theorem of $\sf{ETCG}$ that all the axioms (and theorems) of $\sf{ETCS}$ are satisfied by the category of cogroup objects in any model of $\sf{ETCG}$, which gives you the desired bi-interpretability between $\sf{ETCS}$ and $\sf{ETCG}$. Adding supplementary axioms to $\sf{ETCS}$ (like R) does not change anything.

Corollary: Given $T$ a model of $\sf{ETCS}$, then $Grp(T)$ is a model of $\sf{ETCG}$. Given $A$ a model of $\sf{ETCG}$, then $CoGrp(A)$ is a model of $\sf{ETCS}$. Moreover these two constructions are inverse to each other up to equivalence of categories.

Theorem: The category of co-group objects in the category of groups is equivalent to the category of sets and partial map between then, or equivalently to the category of pointed sets..

(Thanks to Martin Brandenbourgh for pointing out the mistake in an earlier version)

An easy calculation shows that the generators and the units (Edit: that's were the mistake was) are the only elements such that $\mu(y)=y^L*y^R$ and hence that any cogroup morphism comes from a partial function between sets: each generator is sent either to a generator or to the unit.

And with a bit more work, as nicely explained on this other MO answer, one can check that any cogroup object is of this form.

As pointed out by Martin Brandenbourgh in his answer - once we have the category of set and partial maps, (or equivalently the category of pointed sets) one can easily characterize the category of sets and map in purely categorical language: this is the (non-full) subcategory containing all objects and whose maps are the $f:X \to Y$ such that the square obtained by adding the maps $0 \to X$ and $0\to Y$ (where $0$ is the initial object) is a pullback square.

So let's call this the category of "cogroup objects and total maps between them" (were by total, I mean the map that satisfies this pullback condition)

Now, as all this is a theorem of $\sf{ETCS}$, it is a theorem of $\sf{ETCG}$ that all the axioms (and theorems) of $\sf{ETCS}$ are satisfied by the category of "cogroup objects and total maps between them" in any model of $\sf{ETCG}$, which gives you the desired bi-interpretability between $\sf{ETCS}$ and $\sf{ETCG}$. Adding supplementary axioms to $\sf{ETCS}$ (like R) does not change anything.

Corollary: Given $T$ a model of $\sf{ETCS}$, then $Grp(T)$ is a model of $\sf{ETCG}$. Given $A$ a model of $\sf{ETCG}$, then the category $CoGrp(A)^{total}$ of cogroups object and full map between them is a model of $\sf{ETCS}$. Moreover these two constructions are inverse to each other up to equivalence of categories.

(According to the nLab, this is due to Kan, apparently from a paper called "On monoids and their dual")

(According to the nLab, this is due to Kan, from the paper "On monoids and their dual" Bol. Soc. Mat. Mexicana (2) 3 (1958), pp. 52-61, MR0111035)