About double negation and dependent function in Agda

Question

data ⊥ : Set where

f : {A : Set} → {B : A → Set} → ((a : A) → ((B a) → ⊥) → ⊥) → (((a : A) → B a) → ⊥) → ⊥
f = {!   !}

Type of the function f means: If "If you have value (a), then value of (B a) type exists.", then "Function 'If you have value (a), then you have value of (B a) type' exists."

It seems to be true. Because ((P → ⊥) → ⊥) means "In non-constructive mathematics, P holds", and in non-constructive mathematics you can make ((a : A) → B a) from assumption ((a : A) → ((B a) → ⊥) → ⊥).

I tried to prove this but I didn't find any solution. How can I prove it?

Answer 1

It is not provable. This shows that constructive mathematics have much more nuance than you'd expect. This principle is called double negation shift, and it is non-provable for a similar reason as the axiom of choice is non-provable. Actually they look almost the same: AC states that $(x:A)\to \operatorname{non-empty}(B(a))$ implies $\operatorname{non-empty}((x:A)\to B(a))$. This general shifting pattern is also seel with other modalities.