\begin{definition}[Definition:Free Group on Set]
Let $X$ be a set.
A '''free group''' on $X$ is a certain $X$-pointed group, that is, a pair $\struct {F, \iota}$ where:
:$F$ is a group
:$\iota : X \to F$ is a mapping
that can be defined as follows:
\end{definition}