For any set , there is a Group (namely the Free Group)
which contains (a copy of)
and each function where is a group
extends uniquely to a homomorphism
We can make this into a Functor.
Given
define as the unique homomorphism
extending the composite
This is functorial:
Given ,
both and are unique homomorphisms
that extend so they’re equal