stuff.agda

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

module _ {i j} {A : Set i} {B : A -> Set j} where
  -- ∀¬ and ¬∃ are interprovable constructively:
  ¬∃→∀¬ : ¬ (Σ A B) → ∀ a -> ¬ B a;  ¬∃→∀¬ = curry
  ∀¬→¬∃ : (∀ a -> ¬ B a) -> ¬ Σ A B; ∀¬→¬∃ = uncurry

  -- So in particular, ¬∀¬ and ¬¬∃ are interprovable:
  ¬∀¬-to-¬¬∃ : (¬ ∀ (a : A) -> ¬ B a) -> ¬ ¬ Σ A B
  ¬∀¬-to-¬¬∃ ¬all = ¬all ∘ ¬∃→∀¬

  ¬¬∃-to-¬∀¬ : ¬ ¬ Σ A B -> ¬ ∀ (a : A) -> ¬ B a
  ¬¬∃-to-¬∀¬ ¬¬ex = ¬¬ex ∘ ∀¬→¬∃