A Universe of Sorts

We wish to construct the free group on a set $S$ . Call the free group $\Gamma S$ .
Call the forgetful functor from groups to sets as $U$ .
The defining property of the free group is that if we are given a mapping $\phi: S \to UG$ , a map which tells us where the generators go, there is a unique map $\Gamma \phi: \Gamma S \to G$ which maps the generators of the free group via a group homomorphism into $G$ . Further, there is a bijection between $\phi$ and $\Gamma \phi$ .
Written differently, there is a bijection $\hom_\texttt{Set}(S, UG) \simeq \hom_\texttt{Group}(\Gamma S, G)$ . This is the condition for an adjunction.
The idea to construct $\Gamma S$ is roughly, to take all possible maps $f_i: S \to UG$ for all groups $G$ , take the product of all such maps, and define $\Gamma S \equiv im(\pi_i f_i)$ . The details follow.
First off, we can't take all groups, that's too large. So we need to cut down the size somehow. We do this by considering groups with at most $|S|$ generators, since that's all the image of the maps $f_i$ can be anyway. We're only interested in the image at the end, so we can cut down the groups we consider to be set-sized.
Next, we need to somehow control for isomorphisms. So we first take isomorphism classes of groups with at most $|S|$ generators. Call this set of groups $\mathcal G$ We then construct all possible maps $f_i: S \to UG$ for all possible maps $f$ , for all possible $G \in \mathcal G$ .
This lets us construct the product map $f : S \to \prod_{G \in \mathcal G} UG$ given by $f(s) \equiv \prod_{G \in \mathcal G} f_i(s)$ .
Now we define the free group $\gamma S \equiv im(f)$ . Why does this work?
Well, we check the universal property. Suppose we have some map $h: S \to UH$ . This must induce a map $\Gamma h: \Gamma S \to H$ .
We can cut down the map, by writing the map as $h_{im}: S \to im(h)$ . This maps into some subset of $UH$ , from which we can generate a group $H_{im} \subseteq H$ .
First off, there must be some index $k$ such that $f_k = h_{im}$ , since the set of maps $\{ f_i \}$ covers all possible maps from $S$ into groups with those many generators.
This implies we can project the group $\Gamma S$ at the $k$ th index to get a map from $\Gamma S$ into $H_{im}$ .
We can then inject $H_{im}$ into $H$ , giving us the desired map!

§ Weird Free Group Construction from Adjoint Functor Theorem