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}

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}

Binary relations:

\begin{code}

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

\end{code}