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](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 $\mathit{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 $\mathit{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 $\mathit{Grp}$ yet?



Axioms for the category of groups
As requested, here is an answer summarizing axioms for the category of groups that were [given](https://www.cambridge.org/core/journals/canadian-mathematical-bulletin/article/une-caracterisation-de-la-categorie-des-groupes/BDD4B7EA2FD122F7E0F1C81236162FE4) by Pierre Leroux, and which I learned from an MSE answer of Arnaud D. The category of groups is the unique category $C$ with the following properties:


1. It has all limits and colimits, and a zero object.
2. It has as a full subcategory $C\_Z$ a category closed under coproducts and containing a cogroup $Z,$ and generated by the morphisms required by those properties.
3. $C\_Z$ is closed under subobjects in $C.$
4. $Z$ is a regular-projective generator of $C.$
5. Every inclusion of the equivalence class of $0$ in an equivalence relation on an object of $C$ is a normal monomorphism.
6. Every object of $C$ is a subobject of a simple object.


