Isomorphism and validy restriction constructions for cameras.
- It has the same structure as the isomorphism constructions for OFEs, namely, the user of the construction has to give instances of
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.