--- a/CCCGraph1.agda	Thu Mar 26 04:51:54 2020 +0900
+++ b/CCCGraph1.agda	Thu Mar 26 09:30:45 2020 +0900
@@ -46,19 +46,22 @@
    eval1 (f *) g = iv (i (f *)) g
    eval1 (id a) g = i g
 
-   _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    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 g h) = {!!} ・ h -- g  : Arrows a (c <= b)
-   eval < f , g > (iii j h) = {!!}
+   eval ε (iii 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) = iv (eval f g) h
-   eval f (v g) = {!!}
+   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) = {!!}
 
+   _・_ :  {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