--- a/CCCGraph.agda	Sun Apr 28 12:37:34 2019 +0900
+++ b/CCCGraph.agda	Sun Apr 28 13:02:36 2019 +0900
@@ -172,17 +172,27 @@
        IsFunctor.≈-cong isf refl = refl
        IsFunctor.distr isf {a} {b} {c} {g} {f} = extensionality Sets ( λ z → distr {a} {b} {c} {g} {f} z ) 
 
----   record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
----     field
----       cat : Category c₁ c₂ ℓ
----       ccc : CCC cat
----   
----   open CCCObj 
----   
----   record CCCMap  {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
----     field
----       cmap : Functor (cat A ) (cat B )
----       ccf : {A B : CCCObj {c₁} {c₂} {ℓ} } → CCC (cat A) → CCC (cat B)
+---
+---  SubCategoy SC F A is a category with Obj = FObj F, Hom = FMap 
+---
+---     CCC ( SC (CS G)) Sets   have to be proved
+---  SM can be eliminated if we have
+---    sobj (a : vertex g ) → {a}              a set have only a
+---    smap (a b : vertex g ) → {a} → {b}
+
+
+record CCCObj { c₁ c₂ ℓ  : Level} : Set (suc (c₁ ⊔ c₂ ⊔ ℓ)) where
+   field
+     cat : Category c₁ c₂ ℓ
+     ccc : CCC cat
+ 
+open CCCObj 
+ 
+record CCCMap  {c₁ c₂ ℓ : Level} (A B : CCCObj {c₁} {c₂} {ℓ} ) : Set (suc (c₁ ⊔ c₂ ⊔ ℓ )) where
+   field
+     cmap : Functor (cat A ) (cat B )
+     ccf : {A B : CCCObj {c₁} {c₂} {ℓ} } → CCC (cat A) → CCC (cat B)
+
 ---   
 ---   Cart : {c₁ c₂ ℓ : Level} → Category (suc (c₁ ⊔ c₂ ⊔ ℓ)) (suc (c₁ ⊔ c₂ ⊔ ℓ))(suc (c₁ ⊔ c₂ ⊔ ℓ))
 ---   Cart {c₁} {c₂} {ℓ} = record {
@@ -197,14 +207,14 @@
 ---        ; o-resp-≈ = {!!}
 ---        ; associative = {!!}
 ---      }}
----   
----   open import discrete
----   open Graph
----   
----   record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where
----      vmap : vertex x → vertex y
----      emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
----   
+
+open import discrete
+open Graph
+
+record Gmap {v : Level} (x y : Graph {v} ) : Set (suc v) where
+   vmap : vertex x → vertex y
+   emap : {a b : vertex x} → edge x a b → edge y (vmap a) (vmap b)
+
 ---   Grp : {v : Level} → Category (suc v) v v
 ---   Grp {v} = record {
 ---       Obj = Graph {v}