Dense topology <=> double negation operator in a constructive metatheory?

The dense topology for a category $\mathbb{C}$ can be defined as follows, writing $\mathscr{H}:\mathbb{C}\to\widehat{\mathbb{C}}$ for the Yoneda embedding (considering sieves on $c$ as subfunctors of $\mathscr{H}(c)$):

$$J_{\mathsf{dense}}(c) \triangleq \{S\sqsubseteq\mathscr{H}(c) \mid \forall \psi:d\to c.\ \exists \phi:e\to d.\ \psi\circ\phi\in S(e)\}$$

In its logical aspect as a Lawvere-Tierney operator, this topology is said to correspond to the double-negation modality $\lnot\lnot$. I can see how this is the case, by unfolding the meaning of a double negation in the internal language of the presheaf topos into elementary/set-theoretic statements about sieves.

However, I have noticed that this equivalence relies on the De Morgan duality $\lnot\forall x.\lnot P(x) \Leftrightarrow \exists x. P(x)$, which is not constructively valid. That is, if $S$ is a covering sieve for the dense topology, I can certainly show $\lnot\lnot (S = \mathsf{true})$; however, it does not appear to be the case that from $\lnot\lnot(S=\mathsf{true})$, I can constructively conclude that $S$ is a covering sieve for the dense topology.

So, I wonder if the dense topology, formulated in a constructive metatheory (for instance, by replacing the category $\mathbf{Set}$ with some other topos), would in fact correspond to the double-negation modality. It seems like it should not, but this is a bit surprising to me.

P.S. Another question that interests me is whether an alternative formulation of the dense topology (which is constructively the same as the double negation operator) would be useful in a constructive metatheory, and whether it would allow us to do the appropriate constructions.

Addendum: Regarding my P.S. above, I have already noticed a case where the weaker version of the dense topology which is constructively equivalent to the double-negation operator is not sufficient. Specifically, in the case of a Schanuel-like topos, where the atomic topology (which under suitable conditions coincides with the dense topology) is used to induce indexing in "nominal atoms", the weak version of this topology does not appear to be sufficient for establishing the equivalence of the sheaf condition with the existence of unique "strengthenings to the support" for a presheaf (i.e. if $\psi:\Phi\to\Psi$ supports $m:P(\Phi)$, then there exists a unique "strengthening" $m':\Psi$ such that $m'\cdot\psi=m$).

The two topologies are discussed in Coquand's About Goodman's theorem Edit: Coquand shows that the constructive formulation is a topology and suggests that it is not equivalent to the double negation topology. I don't think it is difficult to come up with a Brouwerian counter example. Sorry, I don't have access to the published paper now, as it is behind a paywall.