--- a/CCCGraph.agda	Mon May 11 16:26:35 2020 +0900
+++ b/CCCGraph.agda	Mon May 11 16:47:58 2020 +0900
@@ -21,10 +21,10 @@
 
 postulate extensionality : { c₁ c₂ ℓ : Level} ( A : Category c₁ c₂ ℓ ) → Relation.Binary.PropositionalEquality.Extensionality c₂ c₂
 
-data One  : Set (suc c₁) where
+data One  : Set c₁ where
   OneObj : One   -- () in Haskell ( or any one object set )
 
-sets : CCC (Sets {suc c₁})
+sets : CCC (Sets {c₁})
 sets  = record {
          １  = One
        ; ○ = λ _ → λ _ → OneObj
@@ -95,19 +95,19 @@
                 *-cong refl = refl
 
 open import graph
-module ccc-from-graph  (G : Graph {suc c₁} {suc c₁} )  where
+module ccc-from-graph  (G : Graph {c₁} {c₁} )  where
 
    open import Relation.Binary.PropositionalEquality renaming ( cong to ≡-cong ) hiding ( [_] )
    open Graph
 
-   data Objs : Set (suc c₁) where
+   data Objs : Set c₁ where
       atom : (vertex G) → Objs 
       ⊤ : Objs 
       _∧_ : Objs  → Objs  → Objs 
       _<=_ : Objs → Objs → Objs 
 
-   data  Arrows  : (b c : Objs ) → Set (suc c₁  )
-   data Arrow :  Objs → Objs → Set (suc c₁)  where                       --- case i
+   data  Arrows  : (b c : Objs ) → Set c₁ 
+   data Arrow :  Objs → Objs → Set c₁  where                       --- case i
       arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
       π : {a b : Objs } → Arrow ( a ∧ b ) a
       π' : {a b : Objs } → Arrow ( a ∧ b ) b
@@ -143,7 +143,7 @@
    assoc≡ (iv f f1) g h = cong (λ k → iv f k ) ( assoc≡ f1 g h )
 
    -- positive intutionistic calculus
-   PL :  Category  (suc c₁) (suc c₁)  (suc c₁ )
+   PL :  Category  c₁ c₁ c₁ 
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
@@ -175,7 +175,7 @@
    tr : {a b : vertex G} → edge G a b → ((y : vertex G) → C y a) → (y : vertex G) → C y b
    tr f x y  = graphtocat.next f (x y) 
    
-   fobj :  ( a  : Objs  ) → Set (suc c₁ )
+   fobj :  ( a  : Objs  ) → Set c₁
    fobj  (atom x) = ( y : vertex G ) → C y x
    fobj ⊤ = One
    fobj  (a ∧ b) = ( fobj  a /\ fobj  b)
@@ -197,7 +197,7 @@
 --    Sets is CCC, so we have a cartesian closed category generated by a graph
 --       as a sub category of Sets
 
-   CS :  Functor PL (Sets {suc c₁})
+   CS :  Functor PL (Sets {c₁})
    FObj CS a  = fobj  a
    FMap CS {a} {b} f = fmap  {a} {b} f
    isFunctor CS = isf where
@@ -234,7 +234,7 @@
  
 open CCCObj 
  
-record CCCMap  (A B : CCCObj ) : Set (suc c₁ ) where
+record CCCMap  (A B : CCCObj ) : Set (suc c₁) where
    field
      cmap : Functor (cat A ) (cat B )
      ccf :  CCC (cat A) → CCC (cat B)
@@ -244,7 +244,7 @@
 open  CCCMap
 open import Relation.Binary.Core
 
-Cart :  Category (suc c₁) (suc c₁) (suc c₁)
+Cart :  Category (suc c₁) (suc c₁) (suc c₁) 
 Cart = record {
     Obj = CCCObj 
   ; Hom = CCCMap
@@ -279,13 +279,13 @@
   mrefl : {g : edge C A B} → (eqv : f ≡ g ) → [ C ] f == g
 
 _=m=_ : {C D : Graph {c₁} {c₁} } 
-    → (F G : GMap C D) → Set (suc  c₁)
+    → (F G : GMap C D) → Set (suc c₁)
 _=m=_ {C = C} {D = D} F G = ∀{A B : vertex C} → (f : edge C A B) → [ D ] emap F f == emap G f
 
 _&_ :  {x y z : Graph {c₁} {c₁}} ( f : GMap y z ) ( g : GMap x y ) → GMap x z
 f & g = record { vmap = λ x →  vmap f ( vmap g x ) ; emap = λ x → emap f ( emap g x ) }
 
-Grph :  Category (suc c₁)  (suc c₁) (suc c₁)
+Grph :  Category (suc c₁) (suc c₁)  (suc c₁) 
 Grph  = record {
     Obj = Graph {c₁} {c₁}
   ; Hom = GMap 
@@ -365,10 +365,13 @@
 open ccc-from-graph.Arrows
 open graphtocat.Chain
 
+Sets0 : Category (suc c₁) c₁ c₁
+Sets0 = Sets {c₁}
+
 ccc-graph-univ :  UniversalMapping Grph Cart forgetful.UX 
 ccc-graph-univ = record {
-     F = λ g → csc {!!} ; -- g
-     η = λ a → record { vmap = λ y → {!!} ; emap = λ f x y →  next f (x y) } ; -- graphtocat.Chain a ? ?  
+     F = λ g → csc g ; 
+     η = λ a → record { vmap = λ y → graphtocat.Chain {!!} {!!} {!!} ; emap = λ f x y →  next f (x y) } ; -- graphtocat.Chain a ? ?  
      _* = solution ;
      isUniversalMapping = record {
          universalMapping = {!!} ;
@@ -377,11 +380,11 @@
   } where
        open forgetful  
        open ccc-from-graph
-       csc : Graph {suc c₁} {suc c₁} → Obj Cart  
+       csc : Graph {c₁} {c₁} → Obj Cart  
        csc  g = record { cat = {!!} ; ccc = {!!} ; ≡←≈ = λ eq → eq } 
-       cs :  (g : Graph {suc c₁}{suc c₁} ) → Functor  (ccc-from-graph.PL g) (Sets {suc c₁})
+       cs :  (g : Graph {c₁}{c₁} ) → Functor  (ccc-from-graph.PL g) (Sets {suc c₁})
        cs g = {!!}
-       pl :  (g : Graph {suc c₁} {suc c₁ } ) → Category _ _ _
+       pl :  (g : Graph {c₁} {c₁ } ) → Category _ _ _
        pl g = PL g
        cobj  :   {g : Obj (Grph    )} {c : Obj (Cart)} → Hom Grph g (FObj UX c)  → Objs {!!} → Obj (cat c)
        cobj {g} {c} f (atom x) = vmap f {!!}