The double negation monad on a Heyting Algebra is the monad x ↦ ¬ ¬ x maps-to 𝑥 𝑥 x\mapsto\lnot\lnot x .