Universal property of the free magma

Remarks

Existence: define $h$ by recursion on the construction of elements, with $h(x) = f(x)$ for $x \in X$ and $h(u \cdot v) = h(u) \cdot h(v)$. This recursion is valid because each element of $M(X)$ is either a generator or a product $u \cdot v$ for exactly one pair $(u, v)$. Uniqueness: two homomorphisms that agree on $X$ agree on all elements, by induction on the construction. Example: with $N = (\Z, +)$ and $f(x) = 1$ for all $x$, the homomorphism $h$ sends each element to its number of leaves. With $N = (\N, \max(a, b) + 1)$ and $f(x) = 0$, the homomorphism $h$ sends each element to the height of its binary tree. In Mathlib this is FreeMagma.lift, an equivalence between maps $X \to N$ and magma homomorphisms $M(X) \to N$.

Going deeper

For a student

The proposition says that the free magma is the free algebra of the variety of all magmas. The free semigroup on $X$ has the same kind of universal property, and it is the quotient of $M(X)$ by the congruence generated by associativity. Recursive definitions on binary trees, such as size and height, are instances of this proposition.