[Agda] (Stronger) double negation of law of excluded middle

[Peter Hancock]

Thanks everyone for clarifying "_" for me!

(I often encounter it in types that I make the type-checker guess for me,
rather than figure them out myself.  It's a nuisance, because then
I have to replace it by a hole, and try to persuade Mr. TC that I actually
want to see the thing.)

Back to the main topic, I now appreciate that the original question
was in the context of h-levels and all that jazz.

Let LEM1 be (A : Set)-> someRestriction A -> not not (A or not A)
Let LEM2 be not not ((A : Set)-> someRestriction A -> A or not A)

(where or might be +, or some "propositional" disjunction, if there
is such a thing.)

Then  LEM1 -> LEM2  resembles an instance of DNS (Double Negation Shift):

DNS_{A,P}    ((x : A)-> not not P)  -> not not ((x : A)-> P x)

where A is usually the natural numbers or some small datatype.

I'm pretty sure DNS has been investigated in Kripke semantics.
The ordinary DNS holds in every Kripke model with a finite
frame, apparently.  Since LEM1 is true, this seems to
confirm Paolo's suspicion that an infinitely framed structure
(omega or co-omega) is needed to invalidate LEM2.