[Iris-Club] Two Monoid Questions

[Ralf Jung]

Hi,

> I'm not a fan of leaving lemmas "on the floor" either, but it sounds like this
> issue with bijections is a deathblow to the second proposal (unless I
> misunderstand the conversation above).

It is, but it works fine for your first proposal (with a relation), which
indicates to me that it is the better one. ;)
Libraries will have to work with type aliases and maybe type ascriptions to use
this, but only those libraries that need more freedom than the current auth
offers will really have to do that.  And many of our users anyway tend to define
derive notions for the ownership they need, so the ascriptions will not be
needed in many places.

Kind regards,
Ralf