--- a/CCCGraph.agda	Wed Apr 29 11:24:32 2020 +0900
+++ b/CCCGraph.agda	Thu Apr 30 11:18:11 2020 +0900
@@ -108,7 +108,7 @@
    open import  Relation.Binary.Core 
    open Graph
    
-   data Objs : Set (c₁ ⊔ c₂) where
+   data Objs : Set c₁ where
       atom : (vertex G) → Objs 
       ⊤ : Objs 
       _∧_ : Objs  → Objs  → Objs 
@@ -149,7 +149,7 @@
    associative (iv f f1) g h = cong (λ k → iv f k ) ( associative f1 g h )
 
    -- positive intutionistic calculus
-   PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
+   PL :  Category  c₁  (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
             Obj  = Objs;
             Hom = λ a b →  Arrows  a b ;
@@ -414,9 +414,24 @@
     lemma refl (refl eqv) = mrefl eqv 
 
 
-
-open ccc-from-graph
+open ccc-from-graph.Objs
+open ccc-from-graph.Arrow
+open ccc-from-graph.Arrows
+open graphtocat.Chain
 
---- HX : {c₁ c₂ ℓ : Level} → ( ≈-to-≡ : (A : Category c₁ c₂ ℓ ) →  {a b : Obj A} → {f g : Hom A a b} → A [ f ≈ g ] → f ≡ g  )
----     → Functor (Grph {c₁} {c₂}) (Cart {c₁} {c₂} {ℓ} ) 
---- HX = {!!}
+ccc-graph-univ :  {c₁ : Level } → UniversalMapping (Grph {c₁} {c₁} {c₁ } ) (Cart {c₁} {c₁} {c₁} ) UX
+ccc-graph-univ {c₁}   = record {
+     F = λ g → csc g ;
+     η = λ a → record { vmap = λ y → atom y ; emap = λ f x y →  next f (x y) ; econg = λ eq → econg1 a _ _ eq } ;
+     _* = {!!} ;
+     isUniversalMapping = record {
+         universalMapping = {!!} ;
+         uniquness = {!!}
+      }
+  } where
+       csc : Graph → Obj Cart
+       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))
+       econg1 G f g eq = {!!}