--- a/CCCGraph1.agda	Sun Apr 05 08:59:28 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 09:43:47 2020 +0900
@@ -49,7 +49,11 @@
    eval (iv π' (iv g h)) | < t , t₁ > = t₁
    eval (iv ε (iv g h)) | < t , t₁ > =  iv ε < t , t₁ > 
    eval (iv (f *) (iv g h)) | < t , t₁ > = iv (f *) < t , t₁ > 
-   eval (iv f (iv g h)) | iv f1 t = iv f ( iv f1 t )
+   eval (iv (arrow x) (iv g h)) | iv f1 t = iv (arrow x) (iv f1 t) 
+   eval (iv π (iv g h)) | iv f1 t = iv π (iv f1 t )
+   eval (iv π' (iv g h)) | iv f1 t = iv π' (iv f1 t )
+   eval (iv ε (iv g h)) | iv f1 t = iv ε (iv f1 t )
+   eval (iv (f *) (iv g h)) | iv f1 t = iv (f *) (iv f1 t )
 
    idem-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → f ≡ f1
    idem-<l> refl = refl
@@ -74,9 +78,20 @@
    idem-eval (iv π' (iv g h)) | < t , t₁ > | m = idem-<r> m
    idem-eval (iv ε (iv g h)) | < t , t₁ > | m = cong ( λ k → iv ε k ) m
    idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m = cong ( λ k → iv (f *) k ) m
-   idem-eval (iv f (iv g h)) | iv f1 t | m = lemma where
-       lemma :  eval (iv f (iv f1 t)) ≡ iv f (iv f1 t)
-       lemma = ?
+   idem-eval (iv (arrow x) (iv g h)) | iv f1 (id a) | m = cong ( λ k → iv (arrow x) k ) m
+   idem-eval (iv π (iv g h)) | iv f1 (id a) | m = cong ( λ k → iv π k ) m
+   idem-eval (iv π' (iv g h)) | iv f1 (id a) | m =  cong ( λ k → iv π' k ) m
+   idem-eval (iv ε (iv g h)) | iv f1 (id a) | m = cong ( λ k → iv ε k ) m
+   idem-eval (iv (f *) (iv g h)) | iv f1 (id a) | m = cong ( λ k → iv (f *) k ) m
+   idem-eval (iv (f *) (iv g h)) | iv f1 (○ a) | m = cong ( λ k → iv (f *) k ) m
+   idem-eval (iv (arrow x) (iv g h)) | iv π < t , t₁ > | m = ?
+   idem-eval (iv (arrow x) (iv g h)) | iv π' < t , t₁ > | m = ?
+   idem-eval (iv (arrow x) (iv g h)) | iv ε < t , t₁ > | m = ?
+   idem-eval (iv π (iv g h)) | iv f1 < t , t₁ > | m = {!!}
+   idem-eval (iv π' (iv g h)) | iv f1 < t , t₁ > | m = {!!}
+   idem-eval (iv ε (iv g h)) | iv f1 < t , t₁ > | m = {!!}
+   idem-eval (iv (f *) (iv g h)) | iv f1 < t , t₁ > | m = {!!}
+   idem-eval (iv f (iv g h)) | iv f1 (iv f₁ t) | m = {!!}
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = g