classical.agda

open import Data.Empty
open import Relation.Nullary

infix 0 ⌊_⌋
⌊_⌋ : ∀ {a} → Set a → Set a
⌊ A ⌋ = ¬ ¬ A

pure : ∀ {a} {A : Set a} → A → ⌊ A ⌋
pure x = λ z → z x

_<*>_ : ∀ {a b} {A : Set a} {B : Set b}
      → ⌊ (A → B) ⌋
      → ⌊ A ⌋
      → ⌊ B ⌋
fs <*> xs = λ z → xs (λ z₁ → fs (λ z₂ → z (z₂ z₁)))

_>>=_ : ∀ {a b} {A : Set a} {B : Set b}
      → ⌊ A ⌋
      → (A → ⌊ B ⌋)
      → ⌊ B ⌋
xs >>= f = λ z → xs (λ z₁ → f z₁ z)

open import Data.Sum

lem : ∀ {a} {A : Set a} → ⌊ A ⊎ ¬ A ⌋
lem = λ z → z (inj₂ (λ x → z (inj₁ x)))

_↓_ : ∀ {a} {A : Set a} → ⌊ A ⌋ → A ⊎ ¬ A → A
_ ↓ inj₁ x = x
x ↓ inj₂ y = ⊥-elim (x y)