--- a/CCCGraph1.agda	Sun Apr 05 11:53:00 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 13:00:59 2020 +0900
@@ -85,6 +85,18 @@
    identityR {_} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
    identityR {_} {_} {iv f (iv g h)} = refl
 
+   open import Data.Empty 
+   open import Relation.Nullary 
+
+   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
+   assoc-iv π < f , f₁ > g = refl
+   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 = {!!}
+
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
    ==←≡ eq = cong (λ k → eval k ) eq
 
@@ -113,7 +125,33 @@
                associative (id a) g h = refl
                associative (○ a) g h = refl
                associative (< f , f1 > ) g h = cong₂ ( λ j k → < j , k > ) (associative f g h) (associative f1 g h)
-               associative {a} (iv x f) g h = {!!} 
+               associative {a} (iv π < f , f1 > ) g h = associative f g h
+               associative {a} (iv π' < f , f1 > ) g h = associative f1 g h
+               associative {a} (iv ε < f , f1 > ) g h = cong ( λ k → iv ε k ) ( associative  < f , f1 >  g h )
+               associative {a} (iv (x *) < f , f1 > ) g h = cong ( λ k → iv (x *) k ) ( associative  < f , f1 >  g h )
+               associative {a} (iv x (id _)) g h =  begin
+                       eval (iv x (id _) ・ (g ・ h))
+                    ≡⟨⟩
+                       eval (iv x (g ・ h))
+                    ≡⟨ assoc-iv x g h ⟩
+                       eval (iv x g ・ h)
+                    ≡⟨⟩
+                       eval ((iv x (id _) ・ g) ・ h)
+                    ∎  where open ≡-Reasoning
+               associative {a} (iv x (○ _)) g h =  refl
+               associative {a} (iv x (iv y f)) g h = begin
+                       eval (iv x (iv y f) ・ (g ・ h))
+                    ≡⟨ 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) 
                o-resp-≈  : {A B C : Objs} {f g : Arrows A B} {h i : Arrows B C} →
                             f == g → h == i → (h ・ f) == (i ・ g)