--- a/CCChom.agda	Sat Apr 27 12:17:49 2019 +0900
+++ b/CCChom.agda	Sat Apr 27 12:58:12 2019 +0900
@@ -611,13 +611,13 @@
 
    open Graph
 
-   data Objs (G : Graph ) : Set where
+   data Objs (G : Graph ) : Set where    -- formula
       atom : (vertex G) → Objs G
       ⊤ : Objs G
       _∧_ : Objs G → Objs G → Objs G
       _<=_ : Objs G → Objs G → Objs G
 
-   data Arrow (G : Graph ) :  Objs G → Objs G → Set where
+   data Arrow (G : Graph ) :  Objs G → Objs G → Set where  --- proof
       arrow : {a b : vertex G} →  (edge G) a b → Arrow G (atom a) (atom b)
       ○ : (a : Objs G ) → Arrow G a ⊤
       π : {a b : Objs G } → Arrow G ( a ∧ b ) a
@@ -649,16 +649,16 @@
    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} {.(atom _)} {.(atom _)} (arrow x) = smap G x
-   amap {G} {a} {.⊤} (○ a) _ = OneObj'
-   amap {G} {.(b ∧ _)} {b} π ( x , _) = x
-   amap {G} {.(_ ∧ b)} {b} π'( _ , x) = x
-   amap {G} {.((b <= _) ∧ _)} {b} ε ( f , x ) = f x
-   amap {G} {a} {.(_ ∧ _)} < f , g > x = (amap f x , amap g x)
-   amap {G} {a} {.(_ <= _)} (f *) x = λ y → amap f ( x , y )
+   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} {a} (id a) = λ z → z
-   fmap {G} {a} {b} (next x f ) = Sets [ amap {G} x o fmap f ]
+   fmap {G} {a} (id a) = λ z → z
+   fmap {G} (next x f ) = Sets [ amap {G} x o fmap f ]
 
    --   CS is a map from Positive logic to Sets
    --    Sets is CCC, so we have a cartesian closed category generated by a graph