Intuition.agda

module Intuition where

open import Data.Empty using (⊥)
open import Data.Product using (_,_ ; proj₁ ; proj₂) renaming (_×_ to _∧_)
open import Data.Sum using (inj₁ ; inj₂) renaming (_⊎_ to _∨_)
open import Relation.Nullary using (¬_)

foo : ∀ {a} {A : Set a} → ¬ ¬ (A ∨ ¬ A)
foo x = x (inj₂ (λ y → x (inj₁ y)))

foo′ : ∀ {a} {A : Set a} → ((A ∨ (A → ⊥)) → ⊥) → ⊥
foo′ = foo

bar′ : ∀ {a} {A : Set a} → A ∧ (A → ⊥) → ⊥
bar′ x = proj₂ x (proj₁ x)

bar : ∀ {a} {A : Set a} → ¬ (A ∧ ¬ A)
bar = bar′