Authoritative with fraction
The authoritative CMRA provides a CMRA with a single, authoritative state. Several times now (most recently when @janno asked me about sth. like this today), it seemed useful to allow more than one authoritative state, that all have to be brought together to change it. I just realized that this could be supported by a fairly small change in the authoritative CMRA, namely to replace Ex(M) by Frac * Ag(M):
Auth(M) := { (x, a) \in (Frac * Ag(M))^? * M | ...}The interface would then change to allow a fraction in the ● notation (and once we have an infrastructure for "assertions that can be split at a fraction", it could be registered there). What do you think?