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 

module ccc-from-graph ( Atom : Set ) ( Hom : Atom → Atom → Set ) where

   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )

   data Objs : Set where
      ⊤ : Objs 
      atom : Atom → Objs
      _∧_ : Objs → Objs → Objs
      _<=_ : Objs → Objs → Objs
   
   data Arrow  : Objs → Objs → Set where
      hom : (a b : Atom) →  Hom a b → Arrow (atom a) (atom b)
      id : (a : Objs ) → Arrow a a
      _・_ : {a b c : Objs } → Arrow b c → Arrow a b → Arrow a c 
      ○ : (a : Objs ) → Arrow a ⊤
      π : {a b : Objs } → Arrow ( a ∧ b ) a
      π' : {a b : Objs } → Arrow ( a ∧ b ) b
      <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b) 
      ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )

   record GraphCat : Set where
     field
        identityL : {a b : Objs} {f : Arrow a b } → (id b ・ f) ≡ f
        identityR : {a b : Objs} {f : Arrow a b } → (f ・ id a) ≡ f
        resp : {a b c : Objs} {f g : Arrow a b } {h i : Arrow b c } → f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
        associative : {a b c d : Objs} {f : Arrow c d }{g : Arrow b c }{h : Arrow a b } → (f ・ (g ・ h)) ≡ ((f ・ g) ・ h)


   GLCat :  GraphCat → Category Level.zero Level.zero Level.zero 
   GLCat gc  = record {
    Obj  = Objs ;
    Hom = λ a b →   Arrow a b  ;
    _o_ =  _・_ ; -- λ{a} {b} {c} x y →    ; -- _×_ {c₁ } { c₂} {a} {b} {c} x y ;
    _≈_ =  λ x y → x  ≡ y ;
    Id  =  λ{a} → id a ;
    isCategory  = record {
            isEquivalence =  record {refl = refl ; trans = trans ; sym = sym } 
          ; identityL  = λ{a b f} → GraphCat.identityL gc 
          ; identityR  = λ{a b f} → GraphCat.identityR gc 
          ; o-resp-≈  = λ {a b c f g h i} f=g h=i →  GraphCat.resp gc f=g h=i
          ; associative  = λ{a b c d f g h } → GraphCat.associative gc
       }
    }  
      
   GL :  (gc : GraphCat ) → PositiveLogic (GLCat gc )
   GL _ = record {
         ⊤ = ⊤
       ; ○ = ○
       ; _∧_ =  _∧_
       ; <_,_> = <_,_>
       ; π = π
       ; π' = π'
       ; _<=_ = _<=_
       ; _* = _*
       ; ε = ε
     }

module deduction-theorem (  L :  PositiveLogic A ) where

  open 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 ψ  ・ α ) *