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.

data ∀‘ (A : Set) (B : A → Set) : Set where
  ∀‘i : ((x : A) → B x) → ∀‘ A B

∀‘e : {A : Set} {B : A → Set} (f : ∀‘ A B) → (a : A) → B a
∀‘e (∀‘i f) a = f a

-- We can also identify universal quantifier with Agda's dependent
-- function space (like the implication was identified with the function
-- spaces).

∀-intro :  {A : Set} {B : A → Set} → ((x : A) → B x) → ∀ x → B x
∀-intro f = f

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

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

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

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

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

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

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

∃-elim : {A : Set} → {B : A → Set} → {C : Set} → ((α : A) → B α → C) -> ∃ A B → C
∃-elim d < a , p > = d a p