module LogicalFacts where

infixl  _∘_

open import Logic

_∘_ : {A B : Ω} {C : B → Ω} →
      (∀(b : B) → C b) → ∀(f : A → B) → ∀(a : A) → C(f a)

g ∘ f = λ x → g(f x)


id : {A : Ω} → A → A
id x = x


uncurry : {A B C : Ω} →
  (A → B → C) → A ∧ B → C

uncurry f (∧-intro a b) = f a b


curry : {A B C : Ω} →
  (A ∧ B → C) → A → B → C

curry f a b = f(∧-intro a b)


double-negation-intro : {R A : Ω} →
 A → ((A → R) → R)

double-negation-intro a p = p a


contra-positive : {R A B : Ω} →
 (A → B) → (B → R) → (A → R)

contra-positive f p = p ∘ f


three-negations-imply-one : {R A : Ω} →
  (((A → R) → R) → R) → (A → R)

three-negations-imply-one = contra-positive double-negation-intro


not-exists-implies-forall-not : {R : Ω} → {X : Set} → {A : X → Ω} →
 ((∃ \(x : X) → A x) → R) → ∀(x : X) → A x → R

not-exists-implies-forall-not f x a = f(∃-intro x a)


forall-not-implies-not-exists : {R : Ω} → {X : Set} → {A : X → Ω} →
 (∀(x : X) → A x → R) → (∃ \(x : X) → A x) → R

forall-not-implies-not-exists f (∃-intro x a) = f x a


∃-functor : {X : Set} {A B : X → Ω} →
 ({x : X} → A x → B x) →
 (∃ \(x : X) → A x) →  ∃ \(x : X) → B x

∃-functor f (∃-intro x a) = ∃-intro x (f a)


∃-nested-functor : {X Y : Set} {A B : X → Y → Ω} →
 ({x : X} → {y : Y} → A x y → B x y) →
 (∃ \(x : X) → ∃ \(y : Y) → A x y) →  ∃ \(x : X) → ∃ \(y : Y) → B x y

∃-nested-functor f = ∃-functor (λ a → ∃-functor f a)