[Agda] Double Negation as Monad

[Vag Vagoff]

If constructive mathematics is equivalent to classic one without double
negation elimination law (from wich law of Excluded Middle is derivable)
then constructive mathematics is strictly as  powerful as classic because
simple algorithm may be created which converts classic proofs to
constructive ones automatically using proof continuations and double
negation monad (but converted proof will be surrounded by double negation).

Is this correct?

module DoubleNegationIsMonad where

-- libraries --

data ⊥ : Set where
infix 8 _≡_ ; data _≡_ {A : Set} (a : A) : A → Set where ≡-refl : a ≡ a
infixr 90 _∘_ ; _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → (A → C) ; f
∘ g = λ x → f (g x)
¬_ : (P : Set) → Set ; ¬ P = P → ⊥
¬¬ = λ (p : Set) → ¬ ¬ p

-- helpers --

¬¬-intro : ∀ {P} → P → ¬¬ P
¬¬-intro p = λ f → f p

→¬¬-intro : ∀ {P Q} → (P → Q) → (P → ¬¬ Q)
→¬¬-intro = _∘_ ¬¬-intro

¬¬¬→¬  : ∀ {P} → ¬ ¬ ¬ P → ¬ P
¬¬¬→¬ {P} nnnp = λ p → (¬¬-intro (¬¬-intro p)) nnnp

¬¬¬¬→¬¬  : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P
¬¬¬¬→¬¬ = ¬¬¬→¬

swap : ∀ {P Q} → (P → ¬ Q) → (Q → ¬ P)
swap pq qp p = (pq p) qp

swap&intro : ∀ {P Q} → (P → Q) → ¬  Q → ¬  P
swap&intro = swap ∘ →¬¬-intro

lift : ∀ {P Q} → (P → Q) → ¬¬ P → ¬¬ Q
lift = swap&intro ∘ swap&intro

-- monad --

return : ∀ {P} → P → ¬¬ P
return = ¬¬-intro

infixl 10 _>>=_
_>>=_ : ∀ {P Q} → ¬¬ P → (P → ¬¬ Q)  → ¬¬ Q
ma >>= f = ¬¬¬¬→¬¬ (lift f ma)

join : ∀ {P} → ¬¬ (¬¬ P) → ¬¬ P
join = ¬¬¬¬→¬¬

-- monad laws --

left-identity : ∀ {A B} → (a : A) → (f : A → ¬¬ B) → return a >>= f ≡ f a
left-identity a f = ≡-refl

right-identity : ∀ {A} → (a : ¬¬ A) → a >>= return ≡ a
right-identity a = ≡-refl

associativity : ∀ {A B C} → (a : ¬¬ A) → (b : A → ¬¬ B) → (c : B → ¬¬ C)
→ (a >>= b) >>= c ≡ a >>= (λ x → b x >>= c)
associativity a b c = ≡-refl