--- a/CCCGraph.agda	Fri May 01 17:49:45 2020 +0900
+++ b/CCCGraph.agda	Fri May 01 19:26:54 2020 +0900
@@ -209,35 +209,6 @@
 -- Functor from Positive Logic to Sets
 --
 
-   data SArrow : (a b : Objs) → Set (c₁ ⊔ c₂ ⊔ ℓ) where
-      seq : {a b : vertex G}  → graphtocat.Chain G a b → SArrow (atom a) (atom b)
-      top : {a  : Objs } → SArrow a ⊤
-      pair : {a b c : Objs } → SArrow a b → SArrow a c → SArrow a (b ∧ c )
-      func : {a b c : Objs } → SArrow b c → SArrow a ( c <= b )
-      sid : {a : Objs } → SArrow a a 
-
-   smap :  { a b : Objs  } → Hom PL a b → SArrow (a) (b)
-   samap :  { a b c : Objs  } → Arrow b c  → SArrow (a) (b) → SArrow (a) (c)
-   samap {atom a} (arrow x) sid  = {!!}
-   samap {atom a} (arrow x) (seq y) = seq ( graphtocat.next x y )
-   samap π (pair f g) = f
-   samap π' (pair f g) = g
-   samap ε (pair (func f) g) = {!!}
-   samap (f *) x = func {!!} where
-      f1 : {!!}
-      f1 = smap f
-   samap ε (pair y y₁) = {!!}
-   samap π sid = {!!}
-   samap π' sid = {!!}
-   samap ε sid = {!!}
-   smap (id (atom x)) = seq (graphtocat.id x)
-   smap (id ⊤) = top
-   smap (id (a ∧ b)) = sid -- pair (smap (id a)) (smap (id b))
-   smap (id (b <= a)) = sid 
-   smap (○ a) = top {a}
-   smap < f , g > = pair ( smap f ) (smap g )
-   smap (iv f g ) = samap f ( smap g )
-
    -- open import Category.Sets
    -- postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
@@ -264,23 +235,18 @@
    fmap < f , g > x = ( fmap f x , fmap g x )
    fmap (iv x f) a = amap x ( fmap f a )
 
-   _==_ : { a   : Objs  } → (f g : fobj a ) →  Set ℓ 
-   _==_ {atom x} f g = {!!}
-   _==_ {⊤} OneObj OneObj = OneObj ≡ OneObj
-   _==_ {a ∧ b} (f , g) (h , i) = ( f == h ) /\ ( g == i )
-   _==_ {b <= a} f g = {!!} -- λ (x : fobj a) →  ? -- _≑_ f g {x}
-   
-   _≑_ :  { a  b : Objs  } → (f g : fobj  a → fobj  b ) → {x :  fobj a}  → Set ℓ
-   _≑_ {a} {b} f g {x} = f x == g x
 
 --   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 :  Functor PL (Sets {c₁ ⊔ c₂ ⊔ ℓ})
-   FObj CS a  = fobj  a
-   FMap CS {a} {b} f = fmap  {a} {b} f
-   isFunctor CS = isf where
+   smallGraph : (G : Graph {c₁} { c₂} {ℓ} ) → Set (c₁ ⊔ c₂ ⊔ ℓ)
+   smallGraph G = {b c :  vertex G } → {f h : edge G b c } →  _≅_ G f h  → f ≡ h
+
+   CS :  smallGraph G → Functor PL (Sets {c₁ ⊔ c₂ ⊔ ℓ})
+   FObj (CS sg) a  = fobj  a
+   FMap (CS sg) {a} {b} f = fmap  {a} {b} f
+   isFunctor ( CS sg) = 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)
@@ -293,15 +259,22 @@
            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 = {!!}
+        IsFunctor.≈-cong isf f=g = extensionality Sets ( λ x → lemma _ _ f=g ) where
+           lemma : {a b : Obj PL} → {x : fobj a } → (f g : Hom PL a b ) → PL [ f ≈ g ] → fmap f x ≡ fmap g x
+           lemma f f prefl = refl
+           lemma {a} {⊤} {x} f g p⊤ with fmap f x | fmap g x
+           lemma {a} {⊤} {x} f g p⊤ | OneObj | OneObj = refl
+           lemma (< f , g >) (< h , i >) (<p> f=h g=i) = cong₂ (λ j k → ( j , k ) ) (lemma f h f=h) (lemma g i g=i) 
+           lemma {_} {_} {x} (iv f g) (iv f i) (piv g=i) = cong ( λ k → amap f k ) (lemma g i g=i)
+           lemma (iv (arrow x) f) (iv (arrow y) g) (aiv x=y f=g) = cong₂ ( λ j k → amap (arrow j) k ) (sg x=y ) (lemma f g f=g)
         IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
    open import subcat
 
-   CSC = FCat PL (Sets {c₁ ⊔ c₂ ⊔ ℓ}) CS
+   CSC = λ (gs : smallGraph G) → FCat PL (Sets {c₁ ⊔ c₂ ⊔ ℓ}) (CS gs)
 
-   cc1 : CCC CSC       -- SCS is CCC
-   cc1 = record {
+   cc1 : (gs : smallGraph G) → CCC (CSC gs)      -- SCS is CCC
+   cc1 gs = record {
          １ = ⊤ ;
          ○ =  λ a x → OneObj ;
          _∧_ = λ x y →  x ∧ y   ;
@@ -322,13 +295,13 @@
                *-cong = *-cong
            }
      } where
-        e20 : {a : Obj CSC} {f : Hom CSC a ⊤} (x : fobj a ) → f x ≡ OneObj
+        e20 : {a : Obj (CSC gs) } {f : Hom (CSC gs) a ⊤} (x : fobj a ) → f x ≡ OneObj
         e20 {a} {f} x with f x
         e20 x | OneObj = refl
         π-cong : {a b c : Obj Sets} {f f' : Hom Sets c a} {g g' : Hom Sets c b} →
                     Sets [ f ≈ f' ] → Sets [ g ≈ g' ] → Sets [ (λ x → f x , g x) ≈ (λ x → f' x , g' x) ]
         π-cong refl refl = refl
-        *-cong : {a b c : Obj CSC } {f f' : Hom CSC (a ∧ b) c} →
+        *-cong : {a b c : Obj (CSC gs) } {f f' : Hom (CSC gs) (a ∧ b) c} →
                     Sets [ f ≈ f' ] → Sets [  (λ x y → f (x , y)) ≈ (λ x y → f' (x , y)) ]
         *-cong refl = refl
 
@@ -502,7 +475,7 @@
       }
   } where
        csc : Graph → Obj Cart
-       csc g = record { cat = CSC ; ccc = cc1 } where 
+       csc g = record { cat = CSC {!!} ; ccc = cc1 {!!} } where 
            open ccc-from-graph g
        econg1 : (G : Graph {c₁} {c₁} {c₁}) → { a b : vertex G} → ( f  g : edge G a b ) → _≅_ G f g
           → _≅_ (FObj UX (csc G)) {atom a} {atom b} (λ x y → next f (x y)) (λ x y → next g (x y))