Dan: here's another way to answer your question, which may be more to your taste. You suggest that
- \\(+_1\\) is a way of combining elements from \\(S\\) (?)
- \\(+_2 : \mathbb{N}[S] \times \mathbb{N}[S] \rightarrow \mathbb{N}[S]\\) is the monoidal operation.
However, you don't say what the first operation maps from and more importantly what it maps _to_. If you try to figure this out, you will probably be led to a framework where all you care about is \\(+_2\\). Give it a try! And notice that we can (and should) think of \\(S\\) as a subset of \\(\mathbb{N}[S]\\). So, there's ultimately no point in having a separate operation that only lets you combine elements of \\(S\\).
- \\(+_1\\) is a way of combining elements from \\(S\\) (?)
- \\(+_2 : \mathbb{N}[S] \times \mathbb{N}[S] \rightarrow \mathbb{N}[S]\\) is the monoidal operation.
However, you don't say what the first operation maps from and more importantly what it maps _to_. If you try to figure this out, you will probably be led to a framework where all you care about is \\(+_2\\). Give it a try! And notice that we can (and should) think of \\(S\\) as a subset of \\(\mathbb{N}[S]\\). So, there's ultimately no point in having a separate operation that only lets you combine elements of \\(S\\).
Version 2.1.8p2
