--- a/deductive.agda	Tue Apr 23 06:39:24 2019 +0900
+++ b/deductive.agda	Tue Apr 23 11:30:34 2019 +0900
@@ -18,63 +18,6 @@
          _* : {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