Lemma 1.5.3 (Regularisation). Assuming that:

• $H$ a Heyting algebra

Then

• (1) The subset $H_{\neg \neg }:=\{x\in H:\neg \neg x=x\}$ is a Boolean algebra;
• (2) For every Heyting homomorphism $g:H\to B$ into a Boolean algebra, there is a unique map of Boolean algebras $g_{\neg \neg }:H_{\neg \neg }\to B$ such that $g(x)=g_{\neg \neg }(\neg \neg x)$ for all $x\in H$.