--- a/CCCGraph1.agda	Sat Apr 04 09:41:38 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 04 10:06:20 2020 +0900
@@ -41,6 +41,7 @@
    iv ε < g , g₁ > ・  h = iv ε < g ・ h , g₁ ・ h >
    iv (f *) < g , g₁ > ・ h = iv (f *) < g ・ h , g₁ ・ h > 
    iv f ( (○ a)) ・ g = iv f ( ○ _ )
+   iv x y ・ id a = iv x y
    iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )
    ○ a ・ g = ○ _
    f ・ id b = f
@@ -52,7 +53,13 @@
    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} = {!!}
+   identityR≡ {a} {b} {iv x (id a)} = refl
+   identityR≡ {a} {b} {iv x (○ a)} = refl
+   identityR≡ {a} {_} {iv π < f , g >} = {!!}
+   identityR≡ {a} {b} {iv π' < f , g >} = {!!}
+   identityR≡ {a} {b} {iv ε < f , g >} = {!!}
+   identityR≡ {a} {.(_ <= _)} {iv (x *) < y , y₁ >} = {!!}
+   identityR≡ {a} {b} {iv x (iv f y)} = refl
    identityR : {A B : Objs} {f : Arrows A B} → (f ・ id A) == f
    identityR {a} {b} {f} = cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} )
 
@@ -72,11 +79,37 @@
          ∎  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 = begin
+            iv π < f , f₁ > ・ g
+         ≡⟨⟩
+            f ・ g
+         ≡⟨ sym identityR≡  ⟩
+            (f ・ g) ・ id _
+         ≡⟨⟩
+            iv π < f ・ g , f₁ ・ g > ・ id _
+         ≡⟨ identityR≡  ⟩
+            iv π < f ・ g , f₁ ・ g > 
+         ≡⟨⟩
+            iv π (< f , f₁ > ・ g)
+         ∎  where open ≡-Reasoning
+   assoc-iv π' < f , f₁ > g = begin
+            iv π' < f , f₁ > ・ g
+         ≡⟨⟩
+            f₁ ・ g
+         ≡⟨ sym identityR≡  ⟩
+            (f₁ ・ g) ・ id _
+         ≡⟨⟩
+            iv π' < f ・ g , f₁ ・ g > ・ id _
+         ≡⟨ identityR≡  ⟩
+            iv π' < f ・ g , f₁ ・ g > 
+         ≡⟨⟩
+            iv π' (< f , f₁ > ・ g)
+         ∎  where open ≡-Reasoning
    assoc-iv ε < f , f₁ > g = refl
    assoc-iv (x *) < f , f₁ > g = refl
-   assoc-iv x (iv f f₁) g = {!!}
+   assoc-iv x (iv f f₁) (○ a) = refl
+   assoc-iv x (iv f f₁) < g , g₁ > = refl
+   assoc-iv x (iv f f₁) (iv f₂ g) = refl
 
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
@@ -107,11 +140,13 @@
                       (iv x f ・ (g ・ h)) ・ id a
                     ≡⟨ cong ( λ k → k ・ id a) (assoc-iv x f ( g ・ h )) ⟩
                       iv x (f ・ (g ・ h)) ・ id a
-                    ≡⟨ cong ( λ k → iv x k ・ id a) (≡←== (associative f g _ ) ) ⟩
+                    ≡⟨ cong ( λ k → iv x k ・ id a) (≡←== (associative f g h ) ) ⟩
+                       {!!}
+                    ≡⟨ {!!} ⟩
                       iv x ((f ・ g ) ・ h) ・ id a
-                    ≡⟨ sym (cong ( λ k → k ・ id a) (assoc-iv x (f ・ g ) _))  ⟩
+                    ≡⟨ sym (cong ( λ k → k ・ id a) (assoc-iv x (f ・ g ) h))  ⟩
                       ( iv x (f ・ g ) ・ h) ・ id a
-                    ≡⟨ sym (cong ( λ k → (k ・  h ) ・ id a) (assoc-iv x f _)) ⟩
+                    ≡⟨ sym (cong ( λ k → (k ・  h ) ・ id a) (assoc-iv x f g)) ⟩
                       ((iv x f ・ g) ・ h) ・ id a
                     ∎  where open ≡-Reasoning
                     --  {!!} ( cong ( λ k → iv x k ) ( ≡←== (associative f g h ) ) )