open import Level
open import Category
module deductive {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) where

-- Deduction Theorem

-- positive logic 

record PositiveLogic {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) :  Set ( c₁  ⊔  c₂ ⊔ ℓ ) where
     field
         ⊤ : Obj A 
         ○ : (a : Obj A ) → Hom A a ⊤ 
         _∧_ : Obj A → Obj A → Obj A   
         <_,_> : {a b c : Obj A } → Hom A c a → Hom A c b → Hom A c (a ∧ b)  
         π : {a b : Obj A } → Hom A (a ∧ b) a 
         π' : {a b : Obj A } → Hom A (a ∧ b) b  
         _<=_ : (a b : Obj A ) → Obj A 
         _* : {a b c : Obj A } → Hom A (a ∧ b) c → Hom A a (c <= b) 
         ε : {a b : Obj A } → Hom A ((a <= b ) ∧ b) a 

postulate L :  PositiveLogic A 

⊤ = PositiveLogic.⊤ L
○ = PositiveLogic.○ L
_∧_  = PositiveLogic._∧_  L
<_,_> = PositiveLogic.<_,_> L
π = PositiveLogic.π L
π' = PositiveLogic.π' L
_<=_ = PositiveLogic._<=_ L
_* = PositiveLogic._* L
ε = PositiveLogic.ε L
_・_ = _[_o_] A

-- every proof b →  c with assumption a has following forms

data  φ  {a : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ) where
   i : {b c : Obj A} {k : Hom A b c } → φ x k
   ii : φ x {⊤} {a} x
   iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
   iv : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x ( f ・ g )
   v : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )

α : {a b c : Obj A } → Hom A (( a ∧ b ) ∧ c ) ( a ∧ ( b ∧ c ) )
α = < π  ・ π   , < π'  ・ π  , π'  > >

-- genetate (a ∧ b) → c proof from  proof b →  c with assumption a

kx∈a : {a b c : Obj A } → ( x : Hom A ⊤ a ) → {z : Hom A b c } → ( y  : φ {a} x z ) → Hom A (a ∧ b) c
kx∈a x {k} i = k ・ π'
kx∈a x ii = π
kx∈a x (iii ψ χ ) = < kx∈a x ψ  , kx∈a x χ  >
kx∈a x (iv ψ χ ) = kx∈a x ψ  ・ < π , kx∈a x χ  >
kx∈a x (v ψ ) = ( kx∈a x ψ  ・ α ) *