Can a free group over a set be constructed this way (without equivalence classes of words)? Denote category of monoids equipped with involution by $\textbf{invMon}$.
Objects are pairs $\left(M,\iota\right)$ where $\iota$ is a map
on the underlying set of $M$.
Denoting $\iota$ by $x\mapsto\bar{x}$
we have $\bar{\bar{x}}=x$ and $\overline{x.y}=\bar{y}.\bar{x}$.
Arrows in $\textbf{invMon}$ are homomorphisms that respect
the involution. There is a forgetful functor $U:\textbf{invMon}\rightarrow\textbf{Set}$
and it has a left adjoint $F$.
Every group equipped with the map
$x\mapsto x^{-1}$ can be recognized as object of $\textbf{invMon}$
and every group homomorphism respects this involution. This gives a
functor $I:\textbf{Grp}\rightarrow\textbf{invMon}$
and if $L$ is a left adjoint for $I$ then composite functor $LF:\textbf{Set}\rightarrow\textbf{Grp}$
should sends each set to a group free over the set.
For object $\left(M,\iota\right)$
define $S=\left\{ x.\bar{x}\mid x\in M\right\} $ and $R=\left\{ 1\right\} \times S$.
Let $C$ be the smallest congruence containing $R$ and let $M/C$
denote the 'quotient-monoid'. Then $\left[\bar{x}\right]\left[x\right]=\left[x\right]\left[\bar{x}\right]=\left[1\right]$
showing that $M/C$ is a group with $\left[\bar{x}\right]=\left[x\right]^{-1}$.
So natural map $\nu:M\rightarrow M/C$ respects involution, hence
is an arrow $\nu:\left(M,\iota\right)\rightarrow\left(M/C,inv\right)$
in $\textbf{invMon}$. Also $\left(M/C,\nu\right)$ is universal
in the sence that for every arrow $\psi:\left(M,\iota\right)\rightarrow I\left(G\right)$
in $\textbf{invMon}$ there is a unique group homomorphism $\phi:M/C\rightarrow G$
with $\psi=I\varphi\circ\nu$. This means that $I$ indeed has a left
adjoint.
Then here we have the construction of a free group over a
set that does not mention any equivalence classes of words or any
reduced words. I am very suspicious, however. This because I never
encountered this in literature. 

My question is:

Am I overlooking something?


My second question is:

If it is okay then where can I find it in literature? I can't believe that it is new.

 A: Looks fine. I haven't seen this construction before. Let me summarize it as follows:
We factor $\mathsf{Grp} \to \mathsf{Set}$ as $\mathsf{Grp} \to \mathsf{InvMon} \to  \mathsf{InvSet} \to \mathsf{Set}$.
$\bullet$ The left adjoint of $\mathsf{InvSet} \to \mathsf{Set}$ sends a set $X$ to $X \times \{1\} \cup X \times \{-1\}$ with the involution $(x,1) \leftrightarrow (x,-1)$.  
$\bullet$ The left adjoint of $\mathsf{InvMon} \to \mathsf{InvSet}$ sends a set $X$ with an involution $i$ to the free monoid on $X$ (the set of words over  $X$ equipped with concatenation) with the involution $i(x_1 \dotsc x_n) = i(x_n) \dotsc i(x_1)$.
$\bullet$ The left adjoint of $\mathsf{Grp} \to \mathsf{InvMon}$ maps a monoid $M$ with an involution $i$ to the quotient $M/(x \cdot i(x)=1)_{x \in M}$.
It follows that $\mathsf{Grp} \to \mathsf{Set}$ has a left adjoint, namely the composition of the left adjoints $\mathsf{Set} \to \mathsf{InvSet} \to \mathsf{InvMon} \to \mathsf{Grp}$. This coincides with the usual construction (set of words $x_1^{\pm 1} \dotsc x_n^{\pm 1}$ modulo $x x^{-1} = 1$), but the factorization makes every step trivial, which is very nice.
