What can you say about this type? `forall A B, (forall x:A, notnot (B x)) -> notnot (forall x, B x)`

Is it inhabited, equivalent to some well known axiom, etc

where `Definition notnot A := (A -> False) -> False.`

Isn't it Double-Negation Shift?

It's something like choice, but must be weaker because it follows from excluded middle/double-negation elimination (rather than the other way round).

@James Wood not quite. With `B : A -> Type`

(as opposed to `B : A -> Prop`

) this is not a consequence of excluded middle in Prop.

Last updated: Oct 12 2024 at 12:01 UTC