--- a/CCCGraph1.agda	Sat Apr 04 19:24:14 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 04 20:08:49 2020 +0900
@@ -36,25 +36,38 @@
    eval (id a) = id a
    eval (○ a) = ○ a
    eval < f , f₁ > = < eval f , eval f₁ >
-   eval (iv f g) with eval g
-   eval (iv f g) | id a = iv f (id a)
-   eval (iv f g) | ○ a = iv f ( ○ a )
-   eval (iv π g) | < h , i > = h
-   eval (iv π' g) | < h , i > = i
-   eval (iv f g) | < h , i > = iv f < h , i >
-   eval (iv f g) | iv h i = iv f ( iv h i )
+   eval (iv f (id a)) = iv f (id a)
+   eval (iv f (○ a)) = iv f (○ a)
+   eval (iv π < g , h >) = eval g
+   eval (iv π' < g , h >) = eval h
+   eval (iv ε < g , h >) = iv ε < eval g , eval h >
+   eval (iv (f *) < g , h >) = iv (f *) < eval g , eval h >
+   eval (iv f (iv g h)) with eval (iv g h)
+   eval (iv f (iv g h)) | id a = iv f (id a)  
+   eval (iv f (iv g h)) | ○ a = iv f (○ a)
+   eval (iv π (iv g h)) | < t , t₁ > = t
+   eval (iv π' (iv g h)) | < t , t₁ > = t₁
+   eval (iv f (iv g h)) | < t , t₁ > = iv f < t , t₁ > 
+   eval (iv f (iv g h)) | iv f₁ t = iv f ( iv f₁ t )
 
    idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
    idem-eval (id a) = refl
    idem-eval (○ a) = refl
    idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁)
-   idem-eval (iv f g) with eval g
-   idem-eval (iv f g) | id a = refl
-   idem-eval (iv f g) | ○ a = refl
-   idem-eval (iv π g) | < h , i > = {!!}
-   idem-eval (iv π' g) | < h , i > = {!!}
-   idem-eval (iv f g) | < h , i > = {!!}
-   idem-eval (iv f g) | iv f₁ t = {!!}
+   idem-eval (iv f (id a)) = refl
+   idem-eval (iv f (○ a)) = refl
+   idem-eval (iv π < g , g₁ >) = idem-eval g 
+   idem-eval (iv π' < g , g₁ >) = idem-eval g₁
+   idem-eval (iv ε < f , f₁ >) = cong₂ ( λ j k → iv ε < j , k > ) (idem-eval f) (idem-eval f₁)
+   idem-eval (iv (x *) < f , f₁ >) =  cong₂ ( λ j k → iv (x *) < j , k > ) (idem-eval f) (idem-eval f₁)
+   idem-eval (iv f (iv g h)) with eval (iv g h) | idem-eval (iv g h)
+   idem-eval (iv f (iv g h)) | id a | m = refl
+   idem-eval (iv f (iv g h)) | ○ a | m = refl
+   idem-eval (iv π (iv g h)) | < t , t₁ > | m = {!!}
+   idem-eval (iv π' (iv g h)) | < t , t₁ > | 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 f₁ t | m = {!!}
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = eval g