For \$$\textbf{Free}(G) \$$ to really be a category,
we must check that this data we specified obeys the unitality and associativity properties.
Check that these obeyed.

[Previous](https://forum.azimuthproject.org/discussion/2130)
[Next](https://forum.azimuthproject.org/discussion/2132)

Definition 3.2. To specify a \$$\textit{category C} \$$:

(i) one specifies a collection \$$Ob(\textit{C}) \$$, elements of which are called \$$\textit{objects} \$$.

(ii) for every two objects \$$c, d \$$, one specifies a set \$$C(c, d) \$$, elements of which are called \$$\textit{morphisms} \$$ from \$$c\$$ to \$$d\$$.

(iii) for every object \$$c \in Ob(C) \$$, one specifies a morphism \$$id_c \in C(c, c) \$$, called the \$$\textit{identity morphism} \$$ on \$$c\$$.

(iv) for every three objects \$$c, d, e \in Ob(C) \$$ and morphisms \$$f \in C(c, d) \$$ and \$$g \in C(d, e) \$$,
one specifies a morphism \$$f.g \in C(c, e) \$$, called the composite of \$$f\$$ and \$$g\$$.

It is convenient to denote elements \$$f \in C(c, d) \$$ as \$$f : c \rightarrow d \$$. Here, \$$c\$$ is called the \$$\textit{domain}\$$ of \$$f\$$, and \$$d\$$ is called the \$$\textit{codomain}\$$ of \$$f\$$.

These constituents are required to satisfy two conditions:

(a) **unitality**: for any morphism \$$f : c \rightarrow d \$$, composing with the identities at \$$c\$$ or \$$d\$$
does nothing: \$$id_c . f = f \text{ and } f . id_d = f \$$.

(b) **associativity**: for any three morphisms \$$f : c_0 \rightarrow c_1 , g : c_1 \rightarrow c_2 , \text{ and } h : c_2 \rightarrow c_3 \$$, the following are then equal: \$$( f . g) . h = f . (g . h ) \$$. We can write it simply as \$$f.g.h\$$.