--- a/CCCGraph1.agda	Sun Apr 05 10:02:02 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 10:44:40 2020 +0900
@@ -49,11 +49,7 @@
    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 (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 )
+   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
@@ -92,7 +88,9 @@
    idem-eval (iv ε (iv g h)) | iv ε < t , t₁ > | m =  cong ( λ k → iv ε k ) m
    idem-eval (iv (f *) (iv g h)) | iv ε < t , t₁ > | m =  cong ( λ k → iv (f *) k ) m
    idem-eval (iv (f *) (iv g h)) | iv (f1 *) < t , t₁ > | m =  cong ( λ k → iv (f *) k ) m
-   idem-eval (iv f (iv g h)) | iv f1 (iv f₁ t) | m =   {!!}
+   idem-eval {a} {b} (iv {a} {b} {d} f (iv g h)) | iv {a} {d} {e} f1 (iv {a} {e} {e1} f2 t) | m =  lemma f f1 f2 where
+       lemma : (f : Arrow d b ) → (f1 : Arrow e d ) → (f2 : Arrow e1 e ) → eval (iv f (  iv f1 (iv f2 t))) ≡ iv f ( iv f1 (iv f2 t))
+       lemma f f1 f2 = ?
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = g