Post-facto extensions

We need a mechanism to enhance a given type. For instance,

• to define the monoid of non-negative integers we need the type MONOID and
• to define the exponentiation $(p, n) \longmapsto p^n$ when defining monoids, we need the set of non-negative integers to be defined already.

The solution is to be able

1. to define first the set of non-negative integers without viewing it as a MONOID,
2. then to define the interface MONOID
3. and finally to enhance the concrete class of non-negative integers by adding to it the property of being a MONOID.