--- a/CCCGraph1.agda	Fri Apr 03 16:03:46 2020 +0900
+++ b/CCCGraph1.agda	Fri Apr 03 17:50:48 2020 +0900
@@ -45,21 +45,23 @@
    iv f ( (○ a)) ・ g = iv f ( ○ _ )
    iv f (iv f₁ g) ・ h = iv f (  (iv f₁ g) ・ h )
 
-   eval :  {a b  : Objs } (f : Arrows a b ) → Arrows a b
-   eval ( id a ) = id a
-   eval ( ○ a ) = ○ a
-   eval ( < f , g > ) = <  eval f   , eval g   >
-   eval ( iv f (id _) ) = iv f (id _)
-   eval ( iv π < g , g₁ > ) = eval g 
-   eval ( iv π' < g , g₁ > ) = eval g₁ 
-   eval ( iv ε < g , g₁ > ) = iv ε < eval g  , eval g₁  >
-   eval ( iv (f *) < g , g₁ > ) = iv (f *) < eval g  , eval g₁  > 
-   eval ( iv f ( (○ a)) ) = iv f ( ○ _ )
-   eval ( iv f (iv f₁ g) ) = iv f ( iv f₁ (eval g))
-
    _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
    _==_ {a} {b} x y   = (x  ・ id _ ) ≡ ( y ・ id _ )
 
+   identityR≡ : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
+   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 : Objs} {f : Arrows A B} → (f ・ id A) == f
+   identityR {a} {b} {f} = cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} )
+
+   ≡←== : {A B : Objs} {f g : Arrows A B} → f == g → f ≡ g
+   ≡←== eq = subst₂ (λ j k → j ≡ k ) identityR≡ identityR≡ eq
+
+   ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
+   ==←≡ eq = cong (λ k → k ・ id _) eq
+
    PL :  Category  (c₁ ⊔ c₂) (c₁ ⊔ c₂) (c₁ ⊔ c₂)
    PL = record {
             Obj  = Objs;
@@ -80,27 +82,40 @@
                identityL {_} {_} {○ a} = refl
                identityL {a} {b} {< f , f₁ >} = refl
                identityL {_} {_} {iv f f₁} = refl
-               identityR≡ : {A B : Objs} {f : Arrows A B} → (f ・ id A) ≡ f
-               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 : Objs} {f : Arrows A B} → (f ・ id A) == f
-               identityR {a} {b} {f} = cong ( λ k → k ・ id a ) ( identityR≡ {_} {_} {f} )
+               assoc-iv1 : {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-iv1 (arrow x) f g = ?
+               assoc-iv1 π f g = {!!}
+               assoc-iv1 π' f g = {!!}
+               assoc-iv1 ε f g = {!!}
+               assoc-iv1 (x *) f g = {!!}
+               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 (arrow x) (id .(atom _)) g = {!!}
+               assoc-iv (arrow x) (iv f f₁) g = {!!}
+               assoc-iv π (id .(_ ∧ _)) g = {!!}
+               assoc-iv π < f , f₁ > g = {!!}
+               assoc-iv π (iv f f₁) g = {!!}
+               assoc-iv π' f g = {!!}
+               assoc-iv ε (id .((_ <= _) ∧ _)) g = {!!}
+               assoc-iv ε < f , f₁ > g = {!!}
+               assoc-iv ε (iv f f₁) g = {!!}
+               assoc-iv (x *) f g = {!!}
                associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
                             (f ・ (g ・ h)) == ((f ・ g) ・ h)
                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 = begin
-                       (iv x f ・ (g ・ h)) ・ id a
-                    ≡⟨ {!!} ⟩
-                       iv x ((f ・ (g ・ h)) ・ id a)
-                    ≡⟨  cong ( λ k → iv x k ) ( associative f g h ) ⟩
-                        iv x (((f ・ g) ・ h) ・ id a) 
-                    ≡⟨ {!!} ⟩
-                       ((iv x f ・ g) ・ h) ・ id a
+                      (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 _ ) ) ⟩
+                      iv x ((f ・ g ) ・ h) ・ id a
+                    ≡⟨ sym (cong ( λ k → k ・ id a) (assoc-iv x (f ・ g ) _))  ⟩
+                      ( iv x (f ・ g ) ・ h) ・ id a
+                    ≡⟨ sym (cong ( λ k → (k ・  h ) ・ id a) (assoc-iv x f _)) ⟩
+                      ((iv x f ・ g) ・ h) ・ id a
                     ∎  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)
                o-resp-≈  f=g h=i = {!!}