Skip to content

Instantly share code, notes, and snippets.

@oisdk
Last active January 27, 2019 21:32
Show Gist options
  • Save oisdk/2d6b3c9d33a317ce6ce7f10e58eb68ca to your computer and use it in GitHub Desktop.
Save oisdk/2d6b3c9d33a317ce6ce7f10e58eb68ca to your computer and use it in GitHub Desktop.
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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment