module PredicateLogic where

-- Howard introduced dependent types and could thus extend 
-- Curry's correspondence between propositions as types to the quantifiers

-- Think of 
-- universal quantification (over an infinite set) as infinite conjunction
-- and existential quantification as infinite disjunction

-- The universal quantifier can be defined as a datatype with a single
-- constructor (cf definition of implication)

data ∀‘ (A : Set) (P : A → Set) : Set where
  ∀-intro : ((x : A) → P x) → ∀‘ A P

-- Note that this gives variable free-notation  ∀‘ A P =  ∀‘ A (λ x → P x) for
-- ∀ x : A. P

∀-elim : {A : Set} {P : A → Set} → ∀‘ A P → (a : A) → P a
∀-elim (∀-intro g) a = g a

-- We can also identify the universal quantifier with Agda's dependent
-- function space (like the implication was identified with the function
-- spaces). In Agda you can even write ∀ (x : A) → P or ∀ x → P for (x : A) → P.

-- Existential quantifiers can be defined as Σ-types: a term z : ∃ A P is
-- a (dependent) pair consisting of a witness α : A and a proof p of P α.
-- Note that P is a "predicate".

data ∃ (A : Set) (P : A → Set) : Set where
 <_,_> : (a : A) → P a → ∃ A P

-- The first projection gives access to the "witness" a : A.

witness : {A : Set} {P : A → Set} -> ∃ A P → A
witness < a , p > = a

-- The second projection gives access to the proof that P holds for
-- the witness a (that is, p : P a).

proof : {A : Set} → {P : A → Set} → (c : ∃ A P) → P (witness c)
proof < a , p > = p

-- Existence elimination: d is merely the curried version of (f : ∃ A P → C).

∃-elim : {A : Set} → {P : A → Set} → {Q : Set} → ((a : A) → P a → Q) → ∃ A P → Q
∃-elim f c = f (witness c) (proof c)