--- a/CCCGraph1.agda	Thu Mar 26 16:44:06 2020 +0900
+++ b/CCCGraph1.agda	Thu Mar 26 17:58:51 2020 +0900
@@ -52,17 +52,11 @@
    eval (id _) f = f
    eval π (iii g h) = g
    eval π' (iii g h) = h
-   eval ε (iii (i k) (i h)) = iv (i ε)  < k , h >  
-   eval ε (iii (i k) h) = iv ( iv (i ε) < k , {!!} > ) {!!}
-   eval ε (iii (iv f g) h) = {!!}
-   eval ε (iii (v g) h) = {!!} -- {!!} ・ h -- g  : Arrows a (c <= b)
-   eval < f , g > (iii j h) = iii (eval f (iii j h)) (eval g (iii j h))
-   eval (f *) (iii g h) = {!!}
-   eval f (iv g h) with eval f g
-   ... | i k = eval1 k h
-   ... | k = iv k h
-   eval < f , g > (v h) = iii (eval f (v h)) (eval g (v h))
-   eval (f *) (v g) = {!!}
+   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
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    _・_ {a} {_} {⊤} _ _ = i ( ○ a )