# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1586683100 -32400
# Node ID 07fdaecc17b329481847720d8113ab7d7bf6b9ee
# Parent  32c11e2fdf82e09f3022c3fdef1613bb2b536939
...

diff -r 32c11e2fdf82 -r 07fdaecc17b3 CCCGraph.agda
--- a/CCCGraph.agda	Sun Apr 12 09:57:22 2020 +0900
+++ b/CCCGraph.agda	Sun Apr 12 18:18:20 2020 +0900
@@ -162,54 +162,56 @@
                                     f ≡ g → h ≡ i → (h ・ f) ≡ (i ・ g)
               o-resp-≈ refl refl = refl 
 
-   record SM {v : Level} : Set (suc v)  where
-      field
-        graph : Graph  {v} {v}
-        sobj : vertex graph → Set
-        smap : { a b : vertex graph } → edge graph a b  → sobj a → sobj b
-
-   open SM
-
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-   -- fobj : {G : SM} ( a  : Objs (graph G) ) → Set
-   -- fobj {G} (atom x) = sobj G x
-   -- fobj {G} (a ∧ b) = (fobj {G} a ) /\ (fobj {G} b )
-   -- fobj {G} (a <= b) = fobj {G} b → fobj {G} a
-   -- fobj ⊤ = One
-   -- amap : {G : SM} { a b : Objs (graph G) } → Arrow (graph G) a b → fobj {G} a → fobj {G} b
-   -- amap {G} (arrow x) = smap G x
-   -- amap (○ a) _ = OneObj
-   -- amap π ( x , _) = x
-   -- amap π'( _ , x) = x
-   -- amap ε ( f , x ) = f x
-   -- amap < f , g > x = (amap f x , amap g x)
-   -- amap (f *) x = λ y → amap f ( x , y )
-   -- fmap : {G : SM} { a b : Objs (graph G) } → Hom (DX G) a b → fobj {G} a → fobj {G} b
-   -- fmap {G} {a} (id a) = λ z → z
-   -- fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]
+   data SL : (t : Objs ) → Set  (c₁ ⊔ c₂) where
+      term : SL ⊤
+      type : {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 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 )
+
+   append : { a b : Objs } → SL a → SL b → SL a
+   append f g = {!!}
+
+   fobj : ( a  : Objs  ) → Set (c₁ ⊔ c₂)
+   fobj  a = SL a
+
+   amap : { a b : Objs  } → Arrow  a b → fobj a → fobj b
+   amap (arrow x) a =  x :: a 
+   amap π ( x , y ) = x 
+   amap π' ( x , y ) = y
+   amap ε (func f , x ) = append f x
+   amap (f *) x = func {!!}
+   fmap : { a b : Objs  } → Hom PL a b → fobj a → fobj b
+   fmap (id a) x = x
+   fmap (○ a) x = term
+   fmap < f , g > x = ( fmap f x , fmap g x )
+   fmap (iv x f) a = amap x ( fmap f a )
 
    --   CS is a map from Positive logic to Sets
    --    Sets is CCC, so we have a cartesian closed category generated by a graph
    --       as a sub category of Sets
 
-   -- CS : (G : SM ) → Functor (DX G) (Sets {Level.zero})
-   -- FObj (CS G) a  = fobj a
-   -- FMap (CS G) {a} {b} f = fmap {G} {a} {b} f
-   -- isFunctor (CS G) = isf where
-   --     _++_ = Category._o_ (DX G)
-   --     ++idR = IsCategory.identityR ( Category.isCategory ( DX G ) )
-   --     distr : {a b c : Obj (DX G)}  { f : Hom (DX G) a b } { g : Hom (DX G) b c } → (z : fobj {G} a ) → fmap (g ++ f) z ≡ fmap g (fmap f z)
-   --     distr {a} {b} {c} {f} {next {b} {d} {c} 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 (graph G) d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next x g ) (fmap f z )
-   --        adistr eq x = cong ( λ k → amap x k ) eq
-   --     distr {a} {b} {b} {f} {id b} z =  refl
-   --     isf : IsFunctor (DX G) Sets fobj fmap 
-   --     IsFunctor.identity isf = extensionality Sets ( λ x → refl )
-   --     IsFunctor.≈-cong isf refl = refl
-   --     IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
+   CS : Functor PL (Sets {c₁ ⊔ c₂})
+   FObj CS a  = fobj a
+   FMap CS {a} {b} f = fmap {a} {b} f
+   isFunctor CS = isf where
+        _++_ = 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} {f} {g} z = {!!}  where
+           -- adistr : fmap (g ++ f) z ≡ fmap g (fmap f z) →
+           --     ( x : Arrow d c ) → fmap ( next x (g ++ f) ) z  ≡ fmap ( next 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 )
+        IsFunctor.≈-cong isf refl = refl
+        IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
 
 ------------------------------------------------------