--- a/CCCGraph1.agda	Fri Apr 03 18:44:15 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 04 09:41:38 2020 +0900
@@ -34,9 +34,7 @@
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = g
-   ○ a ・ g = ○ _
    < f , g > ・  h = <  f ・ h  ,  g ・ h  >
-   f ・ id b = f
    iv f (id _) ・ h = iv f h
    iv π < g , g₁ > ・  h = g ・ h
    iv π' < g , g₁ > ・  h = g₁ ・ h
@@ -44,6 +42,8 @@
    iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > 
    iv f ( (○ a)) ・ g = iv f ( ○ _ )
    iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )
+   ○ a ・ g = ○ _
+   f ・ id b = f
 
    _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
    _==_ {a} {b} x y   = (x  ・ id _ ) ≡ ( y ・ id _ )
@@ -52,7 +52,7 @@
    identityR≡ {a} {.a} {id a} = refl
    identityR≡ {a} {⊥} {○ a} = refl
    identityR≡ {a} {_} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) identityR≡  identityR≡  
-   identityR≡ {a} {b} {iv x y} = refl
+   identityR≡ {a} {b} {iv x y} = {!!}
    identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
    identityR {a} {b} {f} = cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} )
 
@@ -63,13 +63,19 @@
    ==←≡ eq = cong (λ k → k ・ id _) eq
 
    assoc-iv : {a b c d : Objs} (x : Arrow c d ) (f : Arrows b c ) ( g : Arrows a b ) → iv x f ・ g ≡ iv x ( f ・ g )
-   assoc-iv x f (id _) = {!!}
-   assoc-iv x (id a) g = {!!}
-   assoc-iv x (○ a) g = {!!}
+   assoc-iv x f (id _) = begin
+            iv x f ・ id _
+         ≡⟨ identityR≡ ⟩
+            iv x f 
+         ≡⟨ sym (cong (λ k → iv x k ) identityR≡) ⟩
+            iv x (f ・ id _)
+         ∎  where open ≡-Reasoning
+   assoc-iv x (id a) g =  refl
+   assoc-iv x (○ a) g = refl
    assoc-iv π < f , f₁ > g = {!!}
    assoc-iv π' < f , f₁ > g = {!!}
-   assoc-iv ε < f , f₁ > g = {!!}
-   assoc-iv (x *) < f , f₁ > g = {!!}
+   assoc-iv ε < f , f₁ > g = refl
+   assoc-iv (x *) < f , f₁ > g = refl
    assoc-iv x (iv f f₁) g = {!!}
 
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)