Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added to double negation topology some of the basic statements (in the section on topos theory)
Added to double negation a proof that it is the unique topology which is both dense and Boolean.
I’ve added some consequences of the interaction between ¬¬ and Aufhebung of ∅⊣* at Aufhebung. This might profit from some expert’s reality check though.
Thomas, in your remark in the entry, why does it follow that
in particular ℰ¬¬=ℰj in case the former is essential
?
ℰj, the Aufhebung of ∅⊣* (which by definition has to be essential - a level), as a dense subtopos is always ℰ¬¬⊆ℰj by general facts on double negation topology, so provided ℰ¬¬ is a level, it always wins out over other (dense) candidates. Lawvere discusses essentiality of ¬¬ as a possible axiom in the Como 1991 paper and ℰ¬¬⊆ℰj occurs in the 1989 ’taco’ paper. What slightly surprises me is that ℰ¬¬=ℰj holds for all cohesive sites and that ℰ¬¬ is the only possible candidate for Boolean Aufhebung of ∅⊣*.
Thanks, now I see what you mean. I have taken the liberty of slightly rephrasing that part in the remark to make it parse unambiguously.
I have also added pointer to p. 8 in Lawvere91 to the relevant remark here at double negation.
1 to 7 of 7