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.

| cite | improve this answer | |
  • $\begingroup$ Thanks for this, Bas! I have accessed Coquand's paper, and it looks very interesting. Just in case anyone else reads this answer and has questions, Coquand notes that the standard formulation of the dense topology is a topology constructively, but does not seem to explicitly comment on whether it is equivalent to double negation. However, in "The space of measurement outcomes as a spectrum for non-commutative algebras" (cs.ox.ac.uk/people/bob.coecke/PDFS/21-Spitters.pdf), Bas remarks that classical metalogic is required to establish the equivalence of this w/ double negation. $\endgroup$ – Jonathan Sterling Dec 24 '16 at 16:05

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.