Certain categories of mathematical structures have had synthetic axiom systems developed for them. One particularly well known such category is the category of sets and functions $Set$, which was axiomatised by William Lawvere as the Elementary Theory of the Category of Sets. More recently, Michael Shulman came up with axioms for the dagger category of sets and relations $Rel$ in his theory Sets, Elements, and Relations, and Chris Heunen and Andre Kornell came up with axioms for the dagger category of (real, complex) Hilbert spaces and continuous linear maps $Hilb$ in their article Axioms for the category of Hilbert spaces. Has anybody developed a synthetic set of axioms for the category of groups $Grp$ yet?

Certain categories of mathematical structures have had synthetic axiom systems developed for them. One particularly well known such category is the category of sets and functions $\mathit{Set}$, which was axiomatised by William Lawvere as the Elementary Theory of the Category of Sets. More recently, Michael Shulman came up with axioms for the dagger category of sets and relations $\mathit{Rel}$ in his theory Sets, Elements, and Relations, and Chris Heunen and Andre Kornell came up with axioms for the dagger category of (real, complex) Hilbert spaces and continuous linear maps $\mathit{Hilb}$ in their article Axioms for the category of Hilbert spaces. Has anybody developed a synthetic set of axioms for the category of groups $\mathit{Grp}$ yet?