Trace Monoid - Universal Property

Universal Property

A dependency morphism (with respect to a dependency D) is a morphism

to some monoid M, such that the "usual" trace properties hold, namely:

1. implies that

2. implies that

3. implies that

4. and imply that

Dependency morphisms are universal, in the sense that for a given, fixed dependency D, if is a dependency morphism to a monoid M, then M is isomorphic to the trace monoid . In particular, the natural homomorphism is a dependency morphism.