In locale theory, one can produce from any locale $A$ its [double negation sublocale](https://ncatlab.org/nlab/show/double+negation#double_negation_locale) $A\_{\neg\neg}$ via the nucleus which maps an open $U$ of $A$ to $\neg \neg U$, which is the interior of the closure of $U$. This quotient frame can be viewed as a sublocale of $A$. For many spaces, such as $\mathbb{R}$, the double-negation sublocale $\mathbb{R}\_{\neg\neg}$ has no points.


For any locales $A$ and $B$, there is a continuous map, which I believe is mono, $$f : (A \times B)\_{\neg\neg} \to A\_{\neg\neg} \times B\_{\neg\neg}.$$


Does this map have a continuous inverse? That is, are these spaces homeomorphic, and does the double-negation operation commute with products? My hunch is that the answer is no. Taking $A$ and $B$ to both be $\mathbb{R}$, the "diagonal" relation on $\mathbb{R}$ should be clopen in $(\mathbb{R} \times \mathbb{R})\_{\neg\neg}$ (in fact, it is equivalent to $\bot$), but I have a feeling that the diagonal of $\mathbb{R}\_{\neg\neg} \times \mathbb{R}\_{\neg\neg}$ shouldn't be open.


If we have probability distributions $\mu\_A : \mathcal{R}(A\_{\neg\neg})$ and $\mu\_B : \mathcal{R}(B\_{\neg\neg})$, then the independent product is $$\mu\_A \otimes \mu\_B : \mathcal{R}(A\_{\neg\neg} \times B\_{\neg\neg}).$$


Under what conditions is this independent product the image of some probability distribution over $\mathcal{R}((A \times B)\_{\neg\neg})$ of the $f$ defined above? That is, when does this product distribution satisfy the (potentially stronger) regularity properties? I think that this is the case when $A$ and $B$ are both $\mathbb{R}$, because I think that for $\mathbb{R}^n$, a probability distribution $\mu$ on $\mathbb{R}^n$ is absolutely continuous with respect to Lebesgue measure if and only if it can be expressed as a distribution over ${\mathbb{R}^n}\_{\neg\neg}$, and since product measures preserve absolute continuity.


I imagine there might be some analogies to be drawn with [Dmitri Pavlov's discussion of measurable spaces in this MathOverflow answer](https://mathoverflow.net/a/49542/82487).



Products of double-negation sublocales (and probability distributions on them)
For your first question, if $X$ and $Y$ are two boolean locale then $X \times Y$ is boolean only if $X$ or $Y$ is discrete. So unless $\neg \neg A$ or $\neg \neg B$ are discrete, $\neg \neg A \times \neg \neg B$ and $\neg \neg (A \times B)$ cannot be isomorphic because one is boolean and the other is not.


For you second question, the answer is yes in a lot a situations, but for completely stupid reasons that will more probably show you that you are not asking the good question: basically all the set you mention in you question are empty !


Indeed, If $A$ is the locale corresponding to a separable metric space with no isolated point, (for example $A =\mathbb{R}$ or $A=\mathbb{R}^n$), then there exist no probability measure on $\neg \neg A$.


In particular probablity measure on $\neg \neg \mathbb{R}$ does not correspond to meansure absolutely continuous with respect to the Lebesgue measure. There is indeed a boolean locale that I'm going to all $\mathbb{R}^{Lebesgue}$ endowed with a morphism to $\mathbb{R}$ such that probability measure on $\mathbb{R}^{Lebesgue}$ corresponds to probablity measure on $\mathbb{R}$ absolutely continuous with respect to the Lebesgue measure but this locale have not much to do with $\neg \neg \mathbb{R}$.


I might be wrong on that, but I don't think that $\mathbb{R}^{Lebesgue}$ is a sublocale of $\mathbb{R}$ (the map to $\mathbb{R}$ is a monomorphism, but I don't think it is an inclusion)


More precisely, $\mathbb{R}^{Lebesgue}$ is exactly the example of pointless topos introduced in SGA4: its opensublocales are the measurable subsets of $\mathbb{R}$ modulo equality almost every where.


