I'm trying to understand the category theoretic proof of free groups. I know a bit of group theory but little category theory. So my strategy has been to (1) first master Michael Barr's proof of free groups, which he claims is modelled after general adjoint functor theorem, but which never leads out of the category of groups; and then (2) study the category-theoretic proof through its relationship to Barr's proof. I've accomplished (1) but am struggling with (2). Barr's proof is simple, and clever. The goal is to show that there is a group F on a set X with map f:X->F such that for any group K with map k:X->K there is a unique homomorphism ø:F->K such that k=ø°f. The strategy is simply to rigorously define the Cartesian product of all groups on X, call it GB, with map gB (B for Big!). We can then define F as the subgroup of GB generated by gB, so that there is inclusion map j from F to GB. We can also define a group Gα with map gα, which has a projection map πα from GB and which has an isomorphism ψ to K. We therefore find a composite homomorphism ø:F->GB->Gα->K, such that k=ψ°πα°j°f. We then prove its uniqueness. I'm having a hard time seeing how that models the category-theoretic proof! I'm slowly starting to understand that we have the forgetful functor U: Grp-->Set which maps a group to its underlying set. Apparently one then proves that this functor is both continuous and satisfies the solution-set conditions. The so-called general adjoint functor theorem (GAFT) apparently then shows that a functor which satisifes these conditions has a left-adjoint, which gives us F: Set-->Grp where F(X) is the free group on X. Apparently this is the free functor which assigns every set S to the free group on S. I understand Barr's proof quite well, but I'm not doing so well with the latter proof in part because I'm failing to see any connections with the former. If anyone can identify any structural connections they can see that would be a great help. Thanks!