Splitting (some of) the laws for persistence into a separate class.
I was wondering if it is possible to split out some of the laws for the persistence modality into a separate class? The reason I am interested in this is because currently there is no way to give a "degenerate" definition of the persistence modality that can be equipped onto an arbitrary BI.
For later, the BI interface includes the operation itself in the signature, and states a bunch of laws that are satisfied by a degenerate instance of the later modality, and the law that is not satisfied by the degenerate version is in a separate class BiLöb
.
Would something like that be possible for the persistence modality?
For example, the laws bi_mixin_persistently_absorbing
and bi_mixin_persistently_and_sep_elim
could be moved into a separate typeclass; then the remaining laws could be satisfied by the identity function.