We may view `unifying s and t' as a property of a subsitution f. (OK, so I really mean a pair of the destination number of variables n and substitution f, but we may safely sweep n under the carpet.)
Also, composition of substitutions induces a `generality' preorder on substitutions: the more you extend a substitution, the less general it becomes. (Should I be saying `comma category' here?)
It makes sense to formulate the higher-order property Max which captures the idea that an arrow (oops, I meant to say substitution) f might be the most general satisfying some property P. So, being a most general unifier is just being a substitution maximal for a Unifier property.
Next: accumulating | Prev: unification as optimisation | Up: contents