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](https://www.ncbi.nlm.nih.gov/pmc/articles/PMC300477/pdf/pnas00186-0196.pdf). More recently, Michael Shulman came up with axioms for the dagger category of sets and relations $Rel$ in his theory [Sets, Elements, and Relations](https://ncatlab.org/nlab/show/SEAR), 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](https://arxiv.org/abs/2109.07418). Has anybody developed a synthetic set of axioms for the category of groups $Grp$ yet?