--- a/CCCGraph1.agda	Sat Apr 11 22:06:02 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 12 03:26:35 2020 +0900
@@ -122,6 +122,15 @@
    iv-e-* (iv f g) | < t , t₁ > = refl
    iv-e-* (iv f g) | iv f₁ t = refl
 
+   iv-e : { a b c : Objs } → (x : Arrow b c ) ( f : Arrows a b) 
+           → { d : Objs } { y : Arrow d b } { g : Arrows a d } → eval f ≡ iv y g 
+           → eval (iv x f) ≡ iv x (eval f)
+   iv-e x (id a) ()
+   iv-e x (○ a) ()
+   iv-e x < f , f₁ > ()
+   iv-e x (iv f g) {_} {y} {h} eq with eval (iv f g) 
+   iv-e x (iv f g) {_} {y} {h} refl | iv y h = refl
+
    π-lemma : {a b c : Objs } → ( g : Arrows a ( b ∧ c ) ) ( f1 : Arrows a b ) ( f2 : Arrows a c )
       → eval g ≡ < f1 , f2 > → eval (iv π g ) ≡ f1
    π-lemma < g , g₁ > f1 f2 refl = refl
@@ -155,7 +164,6 @@
         ∎  where open ≡-Reasoning
    iv-d π (id _) = refl
    iv-d π < g , g₁ > = sym (idem-eval g)
-   iv-d π (iv f (id a)) = refl
    iv-d π (iv x f ) with eval (iv x f) | inspect eval (iv x f)
    ... | id _ | m = refl
    ... | < f1 , f2 > | record {eq = ee } = begin
@@ -167,11 +175,45 @@
         ≡⟨ cong (λ k → eval k ) (π-lemma (iv x f) f1 f2 ee ) ⟩
            eval f1 
         ∎  where open ≡-Reasoning
-   ... | iv x1 f1 | m = {!!}
-   iv-d π (iv f (iv f₁ g)) = {!!}
+   iv-d π (iv x f) | iv x1 f1 | record { eq = ee }  = begin
+           iv π (iv x1 f1)
+        ≡⟨ sym (cong (λ k → iv π k ) ee) ⟩
+           iv π (eval (iv x f))
+        ≡⟨ sym (iv-e π (iv x f) ee )  ⟩
+           eval (iv π (iv x f))
+        ≡⟨ sym (idem-eval (iv π (iv x f))) ⟩
+           eval (eval (iv π (iv x f)))
+        ≡⟨ cong (λ k → eval k ) ( iv-e π (iv x f) ee ) ⟩
+           eval (iv π (eval (iv x f)))
+        ≡⟨ cong (λ k → eval (iv π k)) ee ⟩
+           eval (iv π (iv x1 f1))
+        ∎  where open ≡-Reasoning
    iv-d π' (id _) = refl
    iv-d π' < g , g₁ > = sym (idem-eval g₁)
-   iv-d π' (iv f g) = {!!}
+   iv-d π' (iv x f ) with eval (iv x f) | inspect eval (iv x f)
+   ... | id _ | m = refl
+   ... | < f1 , f2 > | record {eq = ee } = begin
+           f2
+        ≡⟨ sym ( π'-lemma (iv x f) f1 f2 ee ) ⟩
+           eval (iv π' (iv x f))
+        ≡⟨ sym (idem-eval (iv π' (iv x f))) ⟩
+           eval (eval (iv π' (iv x f)))
+        ≡⟨ cong (λ k → eval k ) (π'-lemma (iv x f) f1 f2 ee ) ⟩
+           eval f2 
+        ∎  where open ≡-Reasoning
+   iv-d π' (iv x f) | iv x1 f1 | record { eq = ee }  = begin
+           iv π' (iv x1 f1)
+        ≡⟨ sym (cong (λ k → iv π' k ) ee) ⟩
+           iv π' (eval (iv x f))
+        ≡⟨ sym (iv-e π' (iv x f) ee )  ⟩
+           eval (iv π' (iv x f))
+        ≡⟨ sym (idem-eval (iv π' (iv x f))) ⟩
+           eval (eval (iv π' (iv x f)))
+        ≡⟨ cong (λ k → eval k ) ( iv-e π' (iv x f) ee ) ⟩
+           eval (iv π' (eval (iv x f)))
+        ≡⟨ cong (λ k → eval (iv π' k)) ee ⟩
+           eval (iv π' (iv x1 f1))
+        ∎  where open ≡-Reasoning
    iv-d ε g = begin
             eval (iv ε g)
         ≡⟨ iv-e-ε g ⟩
@@ -209,7 +251,17 @@
    idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m | _ = cong ( λ k → iv (f *) k ) m
    idem-eval (iv ε (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-ε (iv f₁ t)) (cong ( λ k → iv ε k ) m )
    idem-eval (iv (x *) (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-* (iv f₁ t)) (cong ( λ k → iv (x *) k ) m )
-   idem-eval (iv π (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!}
+   idem-eval (iv π (iv g h)) | iv f₁ t | m | record { eq = ee } = begin
+          eval (iv π ( iv f₁ t))
+        ≡⟨ {!!} ⟩
+          eval (iv π (eval (iv g h )))
+        ≡⟨ {!!} ⟩
+          eval (iv π (iv g h)) 
+        ≡⟨ iv-e π (iv g h) ee ⟩
+          iv π (eval (iv g h))
+        ≡⟨ cong (λ k → iv π k ) ee  ⟩
+          iv π ( iv f₁ t)
+        ∎  where open ≡-Reasoning
    idem-eval (iv π' (iv g h)) | iv f₁ t | m | record { eq = ee } = {!!}
    idem-eval (iv (arrow x) (iv g h)) | iv f₁ t | m | record { eq = ee } = trans (iv-e-arrow x (iv f₁ t)) (cong ( λ k → iv (arrow x) k ) m )