Dealing with nested modalities in `iModIntro`
We should support introducing monPred_at P i
. Currently this presents a problem because we already have the following instance:
Global Instance from_modal_monPred_at i P Q 𝓠 :
FromModal modality_id P Q → MakeMonPredAt i Q 𝓠 → FromModal modality_id (P i) 𝓠.
This instance allows introduction of e.g. updates below monPred_at
.
When we add a FromModal
instance for monPred_at P i
, we end up with ambiguity when introducing monPred_at (|==> P) i
: should |==>
or monPred_at
be introduced?
Concretely, we should:
-
Add a FromModal
instance formonPred_at
-
Get the priorities of that instance and e.g. the above from_modal_monPred_at
right -
Do the same for embed