# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1555969164 -32400
# Node ID 6e6c7ad8ea1c066ba6630d9654864915a8e68426
# Parent  6a47f0030adf08184b2500d1155b25c44a32d873
...

diff -r 6a47f0030adf -r 6e6c7ad8ea1c deductive.agda
--- a/deductive.agda	Tue Apr 23 05:12:47 2019 +0900
+++ b/deductive.agda	Tue Apr 23 06:39:24 2019 +0900
@@ -18,36 +18,86 @@
          _* : {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 
+module ccc-from-graph ( Atom : Set ) ( Hom : Atom → Atom → Set ) where
+
+   open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong )
 
-⊤ = PositiveLogic.⊤ L
-○ = PositiveLogic.○ L
-_∧_  = PositiveLogic._∧_  L
-<_,_> = PositiveLogic.<_,_> L
-π = PositiveLogic.π L
-π' = PositiveLogic.π' L
-_<=_ = PositiveLogic._<=_ L
-_* = PositiveLogic._* L
-ε = PositiveLogic.ε L
-_・_ = _[_o_] A
+   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 )
 
--- every proof b →  c with assumption a has following forms
+   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)
+
 
-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 * )
+   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 {
+         ⊤ = ⊤
+       ; ○ = ○
+       ; _∧_ =  _∧_
+       ; <_,_> = <_,_>
+       ; π = π
+       ; π' = π'
+       ; _<=_ = _<=_
+       ; _* = _*
+       ; ε = ε
+     }
 
-α : {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
+module deduction-theorem (  L :  PositiveLogic A ) where
 
-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 ψ  ・ α ) *
+  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 ψ  ・ α ) *