# Sum CMRA / CMRA without core

We would like to support a sensible CMRA structure on sums. For example, we could use a sum CMRA to express `one_shot X`

as `exclC unitC + ag X`

. We could also express the disposable monoid using sums.

Right now, the CMRA structure on sums does not make much sense because both summands need to have a core. It is thus impossible to do a frame-preserving update from `inl a`

to `inr b`

. For sums to work out nicely, we need a way to have summands without a unit.

@robbertkrebbers and me agreed that the most promising way forward is to get rid of the core in the CMRA axioms, and instead add a typeclass for "CMRAs that also have a core". There should not be significant performance trouble because the `iFunctor`

will bundle the core of the user CMRA. The main open question is whether the loss of reflexivity in the CMRA inclusion will be a problem.