--- a/CCCGraph1.agda	Sun Apr 05 17:57:55 2020 +0900
+++ b/CCCGraph1.agda	Mon Apr 06 17:48:24 2020 +0900
@@ -109,6 +109,40 @@
    std-iv ε y (iv z f) ne | iv z1 t = refl
    std-iv (x *) y (iv z f) ne | iv z1 t = refl
 
+   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 (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 {b} {c} {d} g h)) with eval (iv g h) | idem-eval (iv g h)  
+   idem-eval (iv f (iv {_} {_} {d} g h)) | id a | m = refl
+   idem-eval (iv f (iv {_} {_} {d} g h)) | ○ a | m = refl
+   idem-eval (iv π (iv {_} {_} {d} g h)) | < t , t₁ > | m = refl-<l> m
+   idem-eval (iv π' (iv {_} {_} {d} g h)) | < t , t₁ > | m = refl-<r> m
+   idem-eval (iv ε (iv {_} {_} {d} g h)) | < t , t₁ > | m = cong ( λ k → iv ε k ) m
+   idem-eval (iv (f *) (iv {_} {_} {d} g h)) | < t , t₁ > | m = cong ( λ k → iv (f *) k ) m
+   idem-eval (iv f (iv {a} {c} {d} g h)) | iv {a} {c} {d1} f1 t | m with  isnot-∧ d1 | inspect eval (iv g h) 
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv f1 t | m | yes p | record { eq = ee } = lemma where
+      lemma1 :  eval (iv f ( iv f1 t)) ≡ iv f (eval ( iv f1 t))
+      lemma1 =  std-iv f f1 t p
+      lemma : eval (iv f (  iv f1 t)) ≡ iv f ( iv f1 t)
+      lemma = begin
+            eval (iv f (  iv f1 t))
+         ≡⟨ lemma1 ⟩
+            iv f (eval ( iv f1 t))
+         ≡⟨ cong (λ k → iv f k ) m ⟩
+            iv f ( iv f1 t)
+        ∎  where open ≡-Reasoning
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {atom x} f₁ t | m | no ¬p | record { eq = ee } = ⊥-elim ( ¬p (λ ()) )
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {⊤} f₁ t | m | no ¬p | record { eq = ee } =  ⊥-elim ( ¬p (λ ()) )
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {d1 <= d2} f₁ t | m | no ¬p | record { eq = ee } =  ⊥-elim ( ¬p (λ ()) )
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {d1 ∧ d2} f₁ t | m | no ¬p | record { eq = ee } = {!!}
+
    assoc-iv : {a b c d : Objs} (x : Arrow c d) (f : Arrows b c) (g : Arrows a b ) → eval (iv x (f ・ g)) ≡ eval (iv x f ・ g)
    assoc-iv x (id a) g = refl
    assoc-iv x (○ a) g = refl
@@ -116,7 +150,12 @@
    assoc-iv π' < f , f₁ > g = refl
    assoc-iv ε < f , f₁ > g = refl
    assoc-iv (x *) < f , f₁ > g = refl
-   assoc-iv x (iv f g) h = {!!}
+   assoc-iv x (iv f g) h = begin
+            eval (iv x (iv f g ・ h)) 
+        ≡⟨ {!!} ⟩
+            eval (iv x (iv f g) ・ h)
+        ∎  where open ≡-Reasoning
+
 
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
    ==←≡ eq = cong (λ k → eval k ) eq
@@ -165,12 +204,6 @@
                     ≡⟨ sym (assoc-iv x (iv y f) ( g ・ h)) ⟩
                        eval (iv x ((iv y f) ・ (g ・ h)))
                     ≡⟨ {!!}  ⟩
-                       iv x (eval ((iv y f) ・ (g ・ h)))
-                    ≡⟨ {!!}  ⟩
-                       iv x (eval ((iv y f ・ g ) ・ h))
-                    ≡⟨ {!!}  ⟩
-                       eval (iv x ((iv y f ・ g ) ・ h))
-                    ≡⟨ {!!}  ⟩
                        eval ((iv x (iv y f) ・ g) ・ h)
                     ∎  where open ≡-Reasoning
                   -- cong ( λ k → iv x k ) (associative f g h)