Investigate a general definition for free structures

[vikraman]

An idea about how to do it: using ideas from universal algebra, define what a signature is, structure (with operations and equations), homomorphism of structures, and then a free structure over a signature. Then you can define the ♯ operation in a very generic way, and prove the universal property for a general free structure.

As an example, monoids have a signature with two operations {e,⊕}, where e is nullary (takes 0 arguments), and ⊕ is binary (takes 2 arguments). It has 3 equations, where both sides are built up from these two operations. Given just this data about operations and equations, you can define a free monoid inductively. We need to find a good way to encode this generic notion of structure.

We can think about this more after we have a complete example of monoids or comm. monoids worked out.

[vikraman]

We're trying to work out how to go from equations to coherences, so we can go from sets to groupoids.

Equations are a pair of trees on free variables, similarly, coherences should be a pair of sequences of equations on free variables.