How to give "categorical" specifications of categories like Grp?
Here is a possible starting point. $\text{Grp}$, as well as other familiar categories of algebraic objects like $\text{Vect}$ or $\text{Ring}$, are distinguished from arbitrary categories by the fact that they are categories of models of Lawvere theories in $\text{Set}$. This is a categorical way of talking about universal algebra.
A categorical characterization of such categories is known: such categories $C$ must
- be cocomplete
- admit an object $F$ such that $\text{Hom}(F, -)$ preserves sifted colimits and such that every object in $C$ is a sifted colimit of finite coproducts of copies of $F$.
$F$ ends up being the free object on a one-element set, so in the case of $\text{Grp}$ it's $\mathbb{Z}$. Given a fixed choice of $F$, the corresponding Lawvere theory can be taken to be the opposite of the full subcategory of $C$ on the finite coproducts of copies of $F$.
From here the problem becomes characterizing the Lawvere theory of groups among all Lawvere theories.
A closely related fact is that $\text{Grp}, \text{Vect}, \text{Ring}$ are also all monadic over $\text{Set}$, and a categorical characterization of this condition is also known.
If you're willing to work with concrete categories, there's a hack that seems to do what you want. Take $\mathbf{Mon}$ for example. We know that:
- $\mathbf{Mon}$ is a category.
- There's a forgetful functor $U : \mathbf{Set} \leftarrow \mathbf{Mon}$.
There's a natural transformation $\mu:U \Leftarrow U \times U$ that tells us how to multiply the elements of a monoid.
There's a natural transformation $\eta:U \Leftarrow 1$ that tells us what the identity element of each monoid is.
The following hold:
Associativity. For each $X:\mathbf{Mon}$ and all $x,y,z \in UX$, we have $\mu_X(\mu_X(z,y),x) = \mu_X(z,\mu_X(y,x)).$
Unitality. For each $X:\mathbf{Mon}$ and all $x \in UX$, we have $\mu_X(x,\eta(*)) =x$ and $\mu_X(\eta(*),x)$, where $*$ is the unique element of the set $1$.
So by a candidate for the category of monoids, let us mean a category $\mathbf{C}$ together with a forgetful functor $U : \mathbf{Set} \leftarrow \mathbf{C}$ together with two natural transformations $\mu : U \Leftarrow U \times U$ and $\eta : U \Leftarrow 1$, such that the above axioms hold. There's an obvious notion of morphism between such things, and it seems to be the case that $\mathbf{Mon}$ is the terminal candidate for the category of monoids.
This gives us a way of explaining where certain forgetful functors come from. For example, we can view $\mathbf{Ring}$ as a candidate for the category of monoids, so there's a unique morphism $\mathbf{Mon} \leftarrow \mathbf{Ring},$ which is the relevant forgetful functor.