This MR is an alternative to !502 (closed) and subsumes !348 (closed).
The construction for validity restriction in this MR uses more or less the same laws as !502 (closed), but compared to !502 (closed), it has the following advantages:
- It has the same structure as the isomorphism constructions for OFEs, namely, the user of the construction has to give instances of
Op,PCore,Valid,ValidN, and then the construction gives a mixin. - It also works for isomorphisms up to setoid equality instead of just Leibniz equality.
- It actually makes the auth construction shorter. (Not much, since the majority of the work is in proving the rules for validity.)
- It provides the ordinary isomorphism construction (without validity restriction, as in !348 (closed)) as a consequence.