Martin Escardo 2011.

\begin{code}
module CurryHoward where
\end{code}

The universe of propositions is denoted by Prp. By the
Curry-Howard isomorphism, it is the universe of types,
sometimes called sets in Agda.

\begin{code}

open import SetsAndFunctions

Prp = Set

\end{code}

We also need this, where Set₁ is the second universe:

\begin{code}

Prp₁ = Set₁

\end{code}

The false proposition (empty set) is inductively
defined with no cases:

\begin{code}

⊥ : Prp
⊥ = ∅

⊥-elim : {A : Prp} → ⊥ → A
⊥-elim = unique-from-∅

infix   ¬_
infixr  _∧_
infixr  _∨_

¬_ : Prp → Prp
¬ A = (A → ⊥)

_∧_ : Prp → Prp → Prp
A ∧ B = A × B

∧-elim₀ : {A₀ A₁ : Prp} → A₀ ∧ A₁ → A₀
∧-elim₀ = π₀

∧-elim₁ : {A₀ A₁ : Prp} → A₀ ∧ A₁ → A₁
∧-elim₁ = π₁

∧-intro : {A₀ A₁ : Prp} → A₀ → A₁ → A₀ ∧ A₁
∧-intro a₀ a₁ = (a₀ , a₁)

_∨_ : Prp → Prp → Prp
A ∨ B = A + B

∨-intro₀ : {A₀ A₁ : Prp} → A₀ → A₀ ∨ A₁
∨-intro₀ = in₀

∨-intro₁ : {A₀ A₁ : Prp} → A₁ → A₀ ∨ A₁
∨-intro₁ = in₁

∨-elim : {A₀ A₁ B : Prp} →

  (A₀ → B) → (A₁ → B) → A₀ ∨ A₁ → B

∨-elim = cases

∨-commutative : {A B : Prp} → A ∨ B → B ∨ A
∨-commutative = ∨-elim ∨-intro₁ ∨-intro₀


∃ : {X : Set} → (A : X → Prp) → Prp
∃ = Σ


∃-intro : {X : Set} → {A : X → Prp} →

  (x₀ : X) → A x₀ → ∃ \(x : X) → A x

∃-intro x a = (x , a)


∃-witness : {X : Set} {A : X → Prp} →

   (∃ \(x : X) → A x) → X

∃-witness = π₀


∃-elim : {X : Set} {A : X → Prp} →

   (proof : ∃ \(x : X) → A x) → A (∃-witness proof)

∃-elim = π₁


infixr  _↔_

_↔_ : Prp → Prp → Prp
A ↔ B = (A → B) ∧ (B → A)

\end{code}

A set X is inhabited if it has an element, if and only if,
when the set X, considered as a proposition, holds. So the
statement that X is inhabited is X itself! In fact, notice
that X is isomorphic to ∃ \(x : X) → ⊤, where ⊤ is the unit
proposition (assuming extensionality).

\begin{code}

inhabited : Set → Prp
inhabited X = X

\end{code}

Some basic logical facts. 

\begin{code}

contra-positive : {A B : Prp} → (A → B) → ¬ B → ¬ A
contra-positive = contra-variant

\end{code}

Double-negation monad:

\begin{code}

¬¬ : Prp → Prp
¬¬ A = ¬(¬ A)

¬¬-functor : {A B : Prp} → (A → B) → ¬¬ A → ¬¬ B
¬¬-functor = K-functor

double-negation-intro : {A : Prp} → A → ¬¬ A
double-negation-intro = ηK


three-negations-imply-one : {A : Prp} → ¬(¬¬ A) → ¬ A
three-negations-imply-one =
  contra-positive double-negation-intro


not-exists-implies-forall-not : {X : Set} → {A : X → Prp} →

 ¬(∃ \(x : X) → A x) → ∀(x : X) → ¬(A x)

not-exists-implies-forall-not = curry


forall-not-implies-not-exists : {X : Set} → {A : X → Prp} →

 (∀(x : X) → ¬(A x)) → ¬(∃ \(x : X) → A x)

forall-not-implies-not-exists = uncurry

\end{code}

Double-negation unshift:

\begin{code}

DNU : {X : Set} {A : X → Prp} →

 ¬¬(∀ x → A x) → ∀ x → ¬¬(A x)

DNU = KU

\end{code}

Special case, if you like:

\begin{code}

dnu : {A B : Prp} → ¬¬(A ∧ B) → ¬¬ A ∧ ¬¬ B
dnu = ku

\end{code}