The union of the two groups involved in a free product is not quite disjoint $-$ they have to share the same identity element. But otherwise yes, $G*H$ is the free group on $G\cup H$ modulo $1_G=1_H$ and the multiplication tables already in place for $G$ and $H$. Indeed if $G=\langle X|R\rangle$ and $H=\langle Y|S\rangle$ are presentations with $X,Y$ disjoint (by fiat) then $G*H=\langle X\cup Y|R\cup S\rangle$.
In the category of abelian groups the coproduct is the direct sum. This can be obtained from the free product by imposing commutativity: (assuming $G,H$ commutative) we can interpret $G,H$ themselves as subgroups of $G*H$, and we have $G\oplus H= (G*H)/[G,H]$. This is indeed the most free abelian group generated by $G\cup H$ (modulo $1_G=1_H$).
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).)
Best Answer
Since you mentioned in the comments you have, and are familiar with Topology by Munkres, and I think Munkres takes a similar approach to what your question is discussing, I will use it as a guide, and explain some of what is going on there.
So first off, to actually construct an example of a free product of groups, typically you go through this reduced word definition, in which case you need disjoint groups, otherwise there is interaction between subgroups. This is purely convenient for construction, and not necessary for definition of free products (although this is actually what Munkres takes as the definition of free product of groups).
Munkres then defines what it means to be an external free product of $G_\alpha$ relative to monomorphisms $i_\alpha:G_\alpha \to G$ to be when $G$ is a free product of $i_\alpha(G_\alpha)$. Note that he does not require $G_\alpha$ to be disjoint, but by his definition of free product the $i_\alpha(G_\alpha)$ must be disjoint. To show that given $\{G_\alpha\}$ that an external free product always exist, what Munkres does is move to assuming that they are disjoint, which can be done by passing to $\{G_\alpha \times \{\alpha\} \}$ and doing the word construction. Taking this route there are natural monomorphism $j_\alpha:G_\alpha \times \{\alpha \} \to G$, so $G$ is an external free product of this collection, and there are natural isomporphism $\iota_\alpha:G_\alpha \to G_\alpha \times \{\alpha \}$, so $i_\alpha= j_\alpha \iota_\alpha$ is a collection of monomorphisms, and $G$ is in fact an external free product of the $G_\alpha$, and you don't really have to assume the $G_\alpha$ are disjoint, it is just helpful for the actual construction. This "little trick" is frequently used in other places (basically whenever you are constructing things from maps satisfying certain properties), and I think it is one of those things that Munkres, and others would probably expect you to fill or "just know" how to do/it doesn't effect anything.
In a couple of the other answers here, free products is defined in terms of universal property (Munkres uses the term extension condition, or something similar), and note that this does not assume things are disjoint either, for essentially the same reasons as why you don't require the external free product to not be disjoint.
In a little bit more concrete example, if we want to think about $\mathbb{Z} * \mathbb{Z}$ (which is just a name for a group satisfying some universal property) in terms of external free product, we get that there are monomorphisms $i_1,i_2: \mathbb{Z} \to \mathbb{Z} * \mathbb{Z}$ such that $i_1(\mathbb{Z}) \cap i_2(\mathbb{Z})= \{id\}$, and it is a free product $i_1(\mathbb{Z})*i_2(\mathbb{Z})$ in the reduced word sense.
If you look in Munkres I don't think he ever writes anything like $\mathbb{Z} * \mathbb{Z}$, basically because it disagrees with his approach, but from the above example it is pretty easy to see what that would mean, no matter what approach you take to understanding free products.