--- a/CCCGraph.agda	Mon Apr 13 08:10:40 2020 +0900
+++ b/CCCGraph.agda	Mon Apr 13 08:52:35 2020 +0900
@@ -165,31 +165,27 @@
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-   data SL : (t : Objs ) → Set  (c₁ ⊔ c₂) where
-      term : SL ⊤
-      value : (x : vertex G) → SL (atom x)
-      _::_ : {a b : vertex G} → (f : edge G a b ) → (prev : SL (atom a)) → SL (atom b)
-      _,_ : {a b : Objs } → (f : SL a ) → (g : SL b) → SL (a ∧ b)
-      func : {a b : Objs } → ( f : SL a → SL b) → SL (b <= a )    -- tail of f should be a SL a
-
-   _+_ : { a b c : Objs } → ( SL b → SL c ) → ( SL a → SL b ) → SL a → SL c
-   _+_ f g x = f ( g x )
+   record SM : Set (suc (c₁ ⊔ c₂))  where
+      field
+        sobj : vertex G → Set (c₁ ⊔ c₂)
+        smap : { a b : vertex G } → edge G a b  → sobj a → sobj b
+   open SM
 
-   append : { a b : Objs } → SL a → SL b → SL a
-   append f g = {!!}
+   fobj : {G : SM} ( a  : Objs  ) → Set (c₁ ⊔ c₂)
+   fobj {G} (atom x) = sobj G x
+   fobj ⊤ = One
+   fobj {G} (a ∧ b) = ( fobj {G} a /\ fobj {G} b)
+   fobj {G} (a <= b) = fobj {G} b → fobj {G} a
 
-   fobj : ( a  : Objs  ) → Set (c₁ ⊔ c₂)
-   fobj  a = SL a
-
-   fmap : { a b : Objs  } → Hom PL a b → fobj a → fobj b
-   amap : { a b : Objs  } → Arrow  a b → fobj a → fobj b
-   amap (arrow x) a =  x :: a 
+   fmap : {G : SM } { a b : Objs  } → Hom PL a b → fobj {G} a → fobj {G} b
+   amap : {G : SM } { a b : Objs  } → Arrow  a b → fobj {G} a → fobj {G} b
+   amap {G} (arrow x) =  smap G x
    amap π ( x , y ) = x 
    amap π' ( x , y ) = y
-   amap ε (func f , x ) = f x
-   amap (f *) x = func (λ y →  fmap f ( x , y ) )
+   amap ε (f , x ) = f x
+   amap (f *) x = λ y →  fmap f ( x , y ) 
    fmap (id a) x = x
-   fmap (○ a) x = term
+   fmap (○ a) x = OneObj
    fmap < f , g > x = ( fmap f x , fmap g x )
    fmap (iv x f) a = amap x ( fmap f a )
 
@@ -197,19 +193,19 @@
    --    Sets is CCC, so we have a cartesian closed category generated by a graph
    --       as a sub category of Sets
 
-   CS : Functor PL (Sets {c₁ ⊔ c₂})
-   FObj CS a  = fobj a
-   FMap CS {a} {b} f = fmap {a} {b} f
+   CS : {G : SM} → Functor PL (Sets {c₁ ⊔ c₂})
+   FObj (CS {G}) a  = fobj {G} a
+   FMap (CS {G}) {a} {b} f = fmap {G} {a} {b} f
    isFunctor CS = isf where
-        _++_ = Category._o_ PL
+        _+_ = Category._o_ PL
         ++idR = IsCategory.identityR ( Category.isCategory PL )
-        distr : {a b c : Obj PL}  { f : Hom PL a b } { g : Hom PL b c } → (z : fobj  a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
+        distr : {a b c : Obj PL}  { f : Hom PL a b } { g : Hom PL b c } → (z : fobj  a ) → fmap (g + f) z ≡ fmap g (fmap f z)
         distr {a} {a₁} {a₁} {f} {id a₁} z = refl
         distr {a} {a₁} {⊤} {f} {○ a₁} z = refl
         distr {a} {b} {c ∧ d} {f} {< g , g₁ >} z = cong₂ (λ j k  →  j , k  ) (distr {a} {b} {c} {f} {g} z) (distr {a} {b} {d} {f} {g₁} z)
         distr {a} {b} {c} {f} {iv {_} {_} {d} x g} z = adistr (distr  {a} {b} {d} {f} {g} z) x where 
-           adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
-                ( x : Arrow d c ) → fmap ( iv x (g ++ f) ) z  ≡ fmap ( iv x g ) (fmap f z )
+           adistr : fmap (g + f) z ≡ fmap g (fmap f z) →
+                ( x : Arrow d c ) → fmap ( iv x (g + f) ) z  ≡ fmap ( iv x g ) (fmap f z )
            adistr eq x = cong ( λ k → amap x k ) eq
         isf : IsFunctor PL Sets fobj fmap 
         IsFunctor.identity isf = extensionality Sets ( λ x → refl )