This slide just summarises the way we've narrowed the focus from tree-to-tree functions to simultaneous substitutions, then to the concrete datatype of idempotent substitutions.

The embeddings all preserve identity and composition. It's tidy to collect these together in a categorical style.

Next: bounded mgu | Prev: idempotent substitutions | Up: contents