--- a/CCCGraph.agda	Mon Apr 13 08:56:52 2020 +0900
+++ b/CCCGraph.agda	Mon Apr 13 12:22:26 2020 +0900
@@ -165,12 +165,59 @@
    -- 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)
+      func0 : {a b : vertex G } → {c : Objs } →  edge G a b  → SL ( c <= atom b )  → SL (c <= atom a )  
+      func1 : {a b c : Objs } →  SL (b <= a) → SL ( c <= a )  → SL (( b ∧ c) <= a )  
+      func2 : {a b c  : Objs } →  SL ( ( c <= b ) <= a) →  SL ( c <= ( a ∧ b) )  
+      func3 : {a : Objs } → SL ( ⊤ <= a )  
+      func4 : {a : Objs } → SL a → SL ( a <= ⊤  )  
+      func5 : {a b c : Objs } → SL a  → SL ( c <= b ) → SL ( c <= (b <= a) )  
+      func6 : {a b c : Objs } → SL ( b <= a ) → SL ( c <= b ) → SL ( (c <= b )<= a )  
+      func7 : {a : Objs } →  SL ( a <= 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) f = {!!}
+   amap' π (f , f₁) = {!!}
+   amap' π' (f , f₁) = {!!}
+   amap' ε (f , f₁) = {!!}
+   amap' (x *) term = {!!}
+   amap' {atom v} {b <= a} (x *) (value v) = {!!} where
+       lemma : SL a → SL b
+       lemma = λ y → fmap' x ( (value v) , y )
+   amap' (x *) (f :: f₁) = {!!}
+   amap' (x *) (f , f₁) = {!!}
+   amap' (x *) (func0 x₁ f) = {!!}
+   amap' (x *) (func1 f f₁) = {!!}
+   amap' (x *) (func2 f) = {!!}
+   amap' (x *) func3 = {!!}
+   amap' (x *) (func4 f) = {!!}
+   amap' (x *) (func5 f f₁) = {!!}
+   amap' (x *) (func6 f f₁) = {!!}
+   amap' {c} {b <= a} (x *) func7 = {!!} where
+       lemma : SL a → SL b
+       lemma = λ y → fmap' x ( func7 , y )
+   fmap' = {!!}
+
    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
 
+   SSS : SM
+   SSS = record {
+        sobj = λ x →  {!!}
+       ;smap = λ {a} {b} f x → {!!}
+     }
+
    fobj : {G : SM} ( a  : Objs  ) → Set (c₁ ⊔ c₂)
    fobj {G} (atom x) = sobj G x
    fobj ⊤ = One