# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585208646 -32400
# Node ID 3bdb93608aaeaef4d6978b0be69f119493c30ef5
# Parent  b25fcdf3a84a3a704ac203564a0ce6d4a17938ce
...

diff -r b25fcdf3a84a -r 3bdb93608aae CCCGraph1.agda
--- 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