For instance, the theory of monoids gives rise to the generators
zero : AMonoid
+ : AMonoid -> AMonoid -> AMonoid
zero + a = a
a + zero = a
a + (b + c) = (a + b) + c
Unfortunately, nobody is very good at this today. It's a goal to be able to automatically achieve the above system in such a way that isn't O(n^2) effort to encode.