introduce the law of excluded-middle by RAA in Agda

gistfile1.txt

module EM where
{-
See also
http://www.cs.nott.ac.uk/~txa/g53cfr/l06.html/l06.html
-}

open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_)

RAA : Set₁
RAA = {A : Set} -> ¬ ¬ A -> A

-- law of excluded-middle
EM : Set₁
EM = {A : Set} -> A ⊎ (¬ A)

¬¬-EM : {A : Set} -> ¬ (¬ (A ⊎ (¬ A)))
¬¬-EM nnpp = nnpp (inj₂ (λ p → nnpp (inj₁ p)))

RAAtoEM : RAA -> EM
RAAtoEM raa = raa ¬¬-EM