# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1585165914 -32400
# Node ID 9d23caa3864eadd42a8c099be6635e1f2fafb59b
# Parent  a115daa7d30ee2c34c978da1f0c29c9d5a903aec
...

diff -r a115daa7d30e -r 9d23caa3864e CCCGraph1.agda
--- a/CCCGraph1.agda	Thu Mar 26 02:44:48 2020 +0900
+++ b/CCCGraph1.agda	Thu Mar 26 04:51:54 2020 +0900
@@ -33,10 +33,32 @@
       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') 
 
-   eval :  {a b c : Objs } (f : Arrow b c ) → (g : Arrows a b) → Arrows a c
-   eval = {!!}
+   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
 
    _・_ :  {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 (f *) (iii g h) = {!!}
+   eval f (iv g h) = iv (eval f g) h
+   eval f (v g) = {!!}
+
    _・_ {a} {_} {⊤} _ _ = i ( ○ a )
    i (id _)  ・ f = f
    f ・ i (id _)  = f
@@ -44,5 +66,5 @@
    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 ・ g = v ( f ・ iii (iv g π ) (i π') )