[Iris-Club] CMRA structure on uPred

[Ralf Jung]

Hi,

On 29.09.2016 22:30, Robbert Krebbers wrote:
> The proper way of dealing with big operators is to define them in terms
> of a canonical structure for monoids. However, I rather keep the
> algebraic hierarchy as small as possible, and define the big operators
> in terms of CMRAs with units (even if that may be considered an
> engineering hack).

This could be entirely separate from the algebraic hierarchy, and not
increase it at all. (I think I saw this proposed somewhere, but can't
find the source now, so here I'm just echoing someone else.)  I don't
see a good reason why everything you compose with bigops should have a
core and validity, and there are some things you can do already with
just associativity -- tying this to RAs seems rather silly, and even
prevents us from also doing e.g. bigops on conjunction.

Kind regards,
Ralf