Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

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 is the empty set:

\begin{code}

⊥ : Prp
⊥ = ∅

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

infix  50 ¬_
infixr 10 _∧_
infixr 20 _∨_

¬_ : 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 1 _↔_

_↔_ : 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}

Equivalence:

\begin{code}

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

\end{code}

Some basic logical facts.

\begin{code}

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

\end{code}

\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}

Binary relations:

\begin{code}

bin-rel : Set → Prp₁
bin-rel X = X → X → Prp

\end{code}