Royal Road to Free Groups and Free Products This question is more about strategy, which can be used when developing group theory, then about a particular proofs. 
$
\newcommand{GRP}{\mathsf{GRP}}
\newcommand{SET}{\mathsf{SET}}
$
One way to define free group $F_\GRP(A)$ for a set $A$ is to get construct it explicitly as
$$
 F_\GRP(A) = \frac{\bigcup^\infty_{n=0} (A \sqcup A)^n}{(\sim)}
$$
as set of sequences of elements of $A$ with $+1$ or $-1$ sign quotiented by suitable equivalence relation. The bad thing about this approach is that it requires some busy lemmas on words to prove that resulting construction is indeed a group with a desired universal property. 
On the other hand one can use some adjoint functor existence theorems to show that forgotful functor $U_\GRP : \GRP \to \SET $ indeed has a left adjoint which is $F_\GRP$. Now, as I know some category theory, I can use these theorems explicitly instead of inventing ad hoc versions of them. The drawback of this approach is that actual structure of free groups is somewhat obfuscated.
However, in my opinion this is not a problem, as left adjoints preserve colimits, and so I can write 
$$
F_\GRP(A) = F_\GRP\left(\bigsqcup_{a \in A}\{a\} \right) = \coprod_{a \in A} F_{\GRP}\{a\} = \coprod_{a \in A} \mathbb{Z},
$$
where coproduct sign stands for free product. So, to describe free groups I'm left with proving that the free group of the singleton is the countable cyclic group $\mathbb{Z}$, and getting and understanding free products.
But here I'm getting a similar problem, the  constructive definition of free product of  groups $(G_i)_{i \in I}$ is similarly
$$
\coprod_{i \in I} G_i = \frac{\bigcup^\infty_{n=0}\left(\bigsqcup_{i \in I} U_{\GRP} (G_i) \right)^n}{(\sim)},
$$     
which will require similar busy work with finite words. It is OK, and I can do it. But I still want to ask:

Is there an alternative way to define, prove existence and understand structure of free products of groups? I would prefer methods that use category theory to some extension. 

 A: In general, if $\mathcal{A}$ is a variety of algebras and $U : \mathcal{A} \to \mathbf{Sets}$ is the forgetful functor, then we can construct a left adjoint $F : \mathbf{Sets} \to \mathcal{A}$ as follows:


*

*First, take the set of formal expressions built up from atoms corresponding to elements of $X$, using formal counterparts of the operations in $\mathcal{A}$.  (If you're using ZFC as your foundations, you will likely need a set-theoretic argument to show this can be represented by an actual set rather than a proper class.)

*Then, take the quotient by the smallest equivalence relation which contains all instances of relations in $\mathcal{A}$ with formal expressions substituted in, and which also makes all the formal operations be respectful of the equivalence relation.  (It is straightforward to show the class of relations on the set of formal expressions from (1) satisfying these requirements is closed under arbitrary intersections; so then, for example, you could construct the desired equivalence relation as the intersection of all such relations.)
Then, in many cases, it's possible to represent each equivalence class by a member of a restricted class of expressions which is easier to work with; and if we're lucky, we might even be able to choose a canonical such expression in each equivalence class.
In the case $\mathcal{A} = \mathbf{Groups}$, for example, it is easy to show that any formal expression from (1), modulo the equivalence relation in (2), is equivalent to a (possibly empty) product of elements $x \in X$ or $y^{-1}$ for $y \in X$ which together form a reduced word.  You would prove this by "structural induction" on the general formal expression (or, if you prefer, by strong induction on the "total size" of the general formal expression).  The harder part is to show that any two distinct 
reduced words end up in different equivalence classes.
To make this process more concrete in the group case, I think it might help to show how this would be encoded in Coq, where for example (1) is very similar to the way you would define an "abstract syntax tree" type in OCaml or Haskell:
(* formal expressions from (1) *)
Inductive free_group (X:Type) : Type :=
| fg_atom (x:X)
| fg_id
| fg_inv (x : free_group X)
| fg_mul (x y : free_group X).

Arguments fg_atom [X] x.
Arguments fg_id [X].
Arguments fg_inv [X] x.
Arguments fg_mul [X] x y.

(* Equivalence relation described in (2) *)
Inductive fg_equiv (X:Type) : free_group X -> free_group X -> Prop :=
| fg_left_id : forall x : free_group X,
  fg_equiv X (fg_mul fg_id x) x
| fg_right_id : forall x : free_group X,
  fg_equiv X (fg_mul x fg_id) x
| fg_left_inv : forall x : free_group X,
  fg_equiv X (fg_mul (fg_inv x) x) fg_id
| fg_right_inv : forall x : free_group X,
  fg_equiv X (fg_mul x (fg_inv x)) fg_id
| fg_mul_assoc : forall x y z : free_group X,
  fg_equiv X (fg_mul (fg_mul x y) z) (fg_mul x (fg_mul y z))
| fg_equiv_refl : forall x : free_group X,
  fg_equiv X x x
| fg_equiv_sym : forall x y : free_group X,
  fg_equiv X x y -> fg_equiv X y x
| fg_equiv_trans : forall x y z : free_group X,
  fg_equiv X x y -> fg_equiv X y z -> fg_equiv X x z
| fg_equiv_resp_id : fg_equiv X fg_id fg_id
| fg_equiv_resp_inv : forall x x' : free_group X,
  fg_equiv X x x' -> fg_equiv X (fg_inv x) (fg_inv x')
| fg_equiv_resp_mul : forall x x' y y' : free_group X,
  fg_equiv X x x' -> fg_equiv X y y' ->
  fg_equiv X (fg_mul x y) (fg_mul x' y').

(Incidentally, it's also very easy to extend this to describe the group with any given presentation, or in general the object of any variety of algebras with a given presentation: just add the relations from the presentation to the requirements on the equivalence relation in (2).)
