--- a/CCCGraph1.agda	Thu Mar 26 09:30:45 2020 +0900
+++ b/CCCGraph1.agda	Thu Mar 26 16:44:06 2020 +0900
@@ -52,7 +52,10 @@
    eval (id _) f = f
    eval π (iii g h) = g
    eval π' (iii g h) = h
-   eval ε (iii g h) = {!!} -- {!!} ・ h -- g  : Arrows a (c <= b)
+   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