Auth as Views
Gregory suggested a generalization of "Auth" that, in hindsight, seems blatantly obvious: make the authoritative and the fragment not the same type, and let the user pick some relation between them. I think it can truly be any (Coq-level) relation for discrete types; for the CMRA variant we likely need a step-indexed relation. The existing "auth" is then the special case of using the same type, and equality as the relation.
This subsumes !91 (closed) by making the relation also require bijectivity. And this also could be useful for situations where we have a very right CMRA for the fragments, which often means lots of "junk" data (such as to_agree, of ExclBot). So instead of the pattern where we do exists heap, own (● to_auth heap), we could have this to_auth in the relation.
An open question is what would happen with all our theory about local updates.
Things to do:
- Implement a generalized "auth as view" library
- Implement monotone partial bijections (!91 (closed)) in terms of that.