--- a/CCCGraph1.agda	Sat Apr 11 12:07:45 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 11 17:29:45 2020 +0900
@@ -134,13 +134,21 @@
                }
            }  where 
               iv-e : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ iv x (eval g)
-              iv-e = ?
+              iv-e = {!!}
+              iv-e-arrow : { a : Objs } → {b c : vertex G } → (x : edge G b c  ) ( g : Arrows a (atom b) )
+                   → eval (iv (arrow x) g) ≡ iv (arrow x) (eval g)
+              iv-e-arrow x (id (atom _)) = refl
+              iv-e-arrow x (iv f g) with eval (iv f g) 
+              iv-e-arrow x (iv f g) | id (atom _) = refl
+              iv-e-arrow x (iv f g) | iv f₁ t = refl
               iv-d : { a b c : Objs } → (x : Arrow b c ) ( g : Arrows a b ) → eval (iv x g) ≡ eval (iv x (eval g))
               iv-d (arrow x) g = begin
                   eval (iv (arrow x) g) 
-                ≡⟨ {!!} ⟩
+                ≡⟨ iv-e-arrow x g ⟩
                   iv (arrow x) (eval g)
-                ≡⟨ {!!} ⟩
+                ≡⟨ cong (λ k → iv (arrow x) k ) ( sym ( idem-eval g) ) ⟩
+                  iv (arrow x) (eval (eval g))
+                ≡⟨ sym (iv-e-arrow x (eval g)) ⟩
                   eval (iv (arrow x) (eval g))
                 ∎  where open ≡-Reasoning
               iv-d π (id _) = refl