Postulating the LEM in Agda

LEM.agda

module LEM where

open import Data.Empty
open import Data.Product
open import Function
open import Relation.Nullary

∄⇒∀ : {A : Set} {B : A → Set} →
      ¬ (∃ λ a → B a) →
      ∀ a → ¬ (B a)
∄⇒∀ ¬∃ a b = ¬∃ (a , b)

postulate LEM : (A : Set) → Dec A

¬¬A⇒A : {A : Set} → ¬ (¬ A) → A
¬¬A⇒A {A} ¬¬p =
  case LEM A of λ
    { (yes p) → p
    ; (no ¬p) → ⊥-elim $ ¬¬p ¬p
    }

∀̸⇒∃ : {A : Set} {B : A → Set} →
      ¬ (∀ a → B a) →
      ∃ λ a → ¬ (B a)
∀̸⇒∃ {A} {B} ¬∀ = 
  case LEM (∃ λ a → ¬ B a) of λ
    { (yes p) → p
    ; (no ¬p) → ⊥-elim $ ¬∀ (¬¬A⇒A ∘ ∄⇒∀ ¬p)
    }