A notion of CMRA morphims based on the compatibility with validity, core and composition.

The notion of CMRA morphism we have is weird: it only state monotonicity, while there are other properties of CMRAs that are natural to preserve through morphism.

This PR proposes an other notion of morphism, which basically states that morphisms commutes with core and composition. For what we need, this is just more restrictive than what we had before, and this does not add any practical benefit, except that I feel like this notion is more intuitive.

Note that Some used to be a morphism, but no longer is (it does not commutes with the core). However, even though that was proved before, nothing used this.