module Logic where

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

Ω = Set

-- False:

data  : Ω where
-- nothing defined here: there are no constructors of this type.


⊥-elim : {A : Ω}    A
⊥-elim = λ ()


¬_ : Ω  Ω
¬ A = (A  )

infix  50 ¬_

-- True, with proof ⋆:

data  : Ω where
 * : 


data _∧_ (A₀ A₁ : Ω) : Ω where
  ∧-intro : A₀  A₁  A₀  A₁

infixr 10 _∧_


∧-elim₀ : {A₀ A₁ : Ω}  
-------------
 A₀  A₁  A₀
-------------
∧-elim₀ (∧-intro a₀ a₁) = a₀


∧-elim₁ : {A₀ A₁ : Ω}  
-------------
 A₀  A₁  A₁
-------------
∧-elim₁ (∧-intro a₀ a₁) = a₁


data _∨_ (A₀ A₁ : Ω) : Ω where
  ∨-intro₀ : A₀  A₀  A₁
  ∨-intro₁ : A₁  A₀  A₁

infixr 20 _∨_


∨-elim : {A₀ A₁ B : Ω}  
----------------------------------
 (A₀  B)  (A₁  B)  A₀  A₁  B
----------------------------------
∨-elim f₀ f₁ (∨-intro₀ a₀) = f₀ a₀
∨-elim f₀ f₁ (∨-intro₁ a₁) = f₁ a₁


data  {X : Set} (A : X  Ω) : Ω where
     ∃-intro : (x₀ : X)  A x₀   \(x : X)  A x


∃-witness : {X : Set} {A : X  Ω}  
------------------------
  ( \(x : X)  A x)  X
------------------------

∃-witness (∃-intro x a) = x

∃-elim : {X : Set} {A : X  Ω}  
--------------------------------------------------
  (proof :  \(x : X)  A x)  A (∃-witness proof)
--------------------------------------------------
∃-elim (∃-intro x a) = a


-- Some basic logical facts:

_∘_ : {A B : Ω} {C : B  Ω} 
----------------------------------------------------
 (∀(b : B)  C b)  ∀(f : A  B)  ∀(a : A)  C(f a)
----------------------------------------------------
g  f = λ x  g(f x)

infixl 30 _∘_ 


id : {A : Ω}  
------
 A  A
------
id x = x


-- The following is usually used with R=⊥:

contra-positive : {R A B : Ω}  
----------------------------
 (A  B)  (B  R)  (A  R)
----------------------------
contra-positive f p = p  f