--- a/CCCGraph1.agda	Thu Mar 26 17:58:51 2020 +0900
+++ b/CCCGraph1.agda	Thu Apr 02 08:16:17 2020 +0900
@@ -17,54 +17,27 @@
       _∧_ : Objs  → Objs  → Objs 
       _<=_ : Objs → Objs → Objs 
 
-   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where
+   data Arrow :  Objs → Objs → Set (c₁ ⊔ c₂)  where                       --- case i
       arrow : {a b : vertex G} →  (edge G) a b → Arrow (atom a) (atom b)
       ○ : (a : Objs ) → Arrow a ⊤
       π : {a b : Objs } → Arrow ( a ∧ b ) a
       π' : {a b : Objs } → Arrow ( a ∧ b ) b
       ε : {a b : Objs } → Arrow ((a <= b) ∧ b ) a
-      <_,_> : {a b c : Objs } → Arrow c a → Arrow c b → Arrow c (a ∧ b)
-      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )
-      id : ( a : Objs ) → Arrow a a
+      _* : {a b c : Objs } → Arrow (c ∧ b ) a → Arrow c ( a <= b )        --- case v
 
    data  Arrows  : (b c : Objs ) → Set ( c₁  ⊔  c₂ ) where
-      i   : {b c : Objs} (k : Arrow b c ) → Arrows b c
-      iii : {b c' c'' : Objs } ( f : Arrows b c' ) ( g : Arrows b c'' ) → Arrows b (c'  ∧ c'')  
-      iv  : {b c d : Objs } ( f : Arrows d c ) ( g : Arrow b d ) → Arrows b c
-      v   : {b c' c'' : Objs } ( f : Arrows (b ∧ c') c'' ) → Arrows b (c'' <= c') 
-
-   eval1 :  {a b c : Objs } (f : Arrow b c ) → (g : Arrow a b) → Arrows a c
-   eval1 {a} {_} {⊤} _ _ = i ( ○ a )
-   eval1 f (id a)  = i f
-   eval1 (arrow x) g = iv (i (arrow x)) g
-   eval1 π < f , g > = i f
-   eval1 π g = iv (i π) g
-   eval1 π' < f , g > = i g
-   eval1 π' g = iv (i π') g
-   eval1 ε g = iv (i ε) g
-   eval1 < f , g > h = iv (i < f , g >) h
-   eval1 (f *) g = iv (i (f *)) g
-   eval1 (id a) g = i g
-
-   eval :  {a b c : Objs } (f : Arrow b c ) → (g : Arrows a b) → Arrows a c
-   eval {a} {_} {⊤} _ _ = i ( ○ a )
-   eval f (i k) = eval1 f k
-   eval (id _) f = f
-   eval π (iii g h) = g
-   eval π' (iii g h) = h
-   eval ε (iii (i f) (i g )) = iv (i ε) < f , g >
-   eval ε (iii f g ) = {!!}
-   eval < f , g > h = iii (eval f h) (eval g h)
-   eval (f *) g = v (eval f (iii (iv g π ) (i π') )) 
-   eval f (iv g h) = iv (eval f g) h
+      id : ( a : Objs ) → Arrows a a                                      --- case i
+      <_,_> : {a b c : Objs } → Arrows c a → Arrows c b → Arrows c (a ∧ b)   --- case iii
+      iv  : {b c d : Objs } ( f : Arrow d c ) ( g : Arrows b d ) → Arrows b c   -- cas iv
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
-   _・_ {a} {_} {⊤} _ _ = i ( ○ a )
-   i (id _)  ・ f = f
-   f ・ i (id _)  = f
-   (iv f g) ・ h  = f ・ eval g h 
-   f ・ (iv g h)  = iv ( f ・ g ) h
-   i f ・ g = eval f g 
-   iii f g ・  h = iii (f ・ h) ( g ・ h )
-   v f ・ g = v ( f ・ iii (iv g π ) (i π') )  
+   _・_ {a} {b} {⊤} _ _ = iv (○ a) (id a)
+   id a ・ g = g
+   < f , g > ・  h = < ( f ・ h ) , ( g ・ h ) >
+   iv f (id _) ・ h = iv f h
+   iv π < g , g₁ > ・  h = g ・ h
+   iv π' < g , g₁ > ・  h = g₁ ・ h
+   iv ε < g , g₁ > ・  h = iv ε < g ・ h , g₁ ・ h >
+   iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > -- Arrows b a Arrows a b
+   iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )