In the answer provided to the question https://mathoverflow.net/questions/296440/modal-collapse-upon-addition-of-the-law-of-the-excluded-middle-to-an-intuitionis, a proof is given, showing that a modality $\bigcirc$ becomes trivial if we assume that the law of the excluded middle is true. Part of the proof assumes that the law of the excluded middle and double negation elimination are equivalent:
$$\neg(\neg M\wedge\bigcirc M)$$ By de Morgan and law of excluded middle, $$M\vee \neg\bigcirc M$$ So, $$\bigcirc M\to M$$
In the logic HYPE, discussed recently in https://link.springer.com/article/10.1007/s10992-018-9467-0 and https://link.springer.com/article/10.1007/s10992-020-09558-5, the law of the excluded middle fails but double negation elimination and De Morgan laws hold, and I am wondering whether $\bigcirc$ is trivial in this logic, using the proof given in the answer cited, and without assuming the law of the excluded middle in the proof.
I presume it does, because the step from $\neg(\neg M\wedge\bigcirc M)$ to $M\vee \neg\bigcirc M$ is by double negation elimination and the de Morgan laws.
This would then show that a lax modality cannot be combined with HYPE.
Actually, in HYPE:
$\not\vdash \bot \leftrightarrow A \land \neg A$
Since the proof given here https://mathoverflow.net/questions/296440/modal-collapse-upon-addition-of-the-law-of-the-excluded-middle-to-an-intuitionis involves substituting $\bot$ with $M \land \neg M$, then it can't go through in HYPE, but perhaps there is another proof which shows that HYPE cannot be combined with $\bigcirc$