--- a/CCCGraph1.agda	Sun Apr 05 09:43:47 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 10:02:02 2020 +0900
@@ -78,20 +78,21 @@
    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 (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 (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 = {!!}
+   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 f (iv g h)) | iv π < t , t₁ > | m = {!!}
+   idem-eval (iv f (iv g h)) | iv π' < t , t₁ > | m = {!!}
+   idem-eval (iv (arrow x) (iv g h)) | iv ε < t , t₁ > | m = cong ( λ k → iv (arrow x) k ) m
+   idem-eval (iv π (iv g h)) | iv ε < t , t₁ > | m = cong ( λ k → iv π k ) m
+   idem-eval (iv π' (iv g h)) | iv ε < t , t₁ > | m =  cong ( λ k → iv π' k ) m
+   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 =   {!!}
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = g