--- a/CCCGraph1.agda	Sat Apr 04 20:08:49 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 08:59:28 2020 +0900
@@ -47,8 +47,15 @@
    eval (iv f (iv g h)) | ○ a = iv f (○ a)
    eval (iv π (iv g h)) | < t , t₁ > = t
    eval (iv π' (iv g h)) | < t , t₁ > = t₁
-   eval (iv f (iv g h)) | < t , t₁ > = iv f < t , t₁ > 
-   eval (iv f (iv g h)) | iv f₁ t = iv f ( iv f₁ t )
+   eval (iv ε (iv g h)) | < t , t₁ > =  iv ε < t , t₁ > 
+   eval (iv (f *) (iv g h)) | < t , t₁ > = iv (f *) < t , t₁ > 
+   eval (iv f (iv g h)) | iv f1 t = iv f ( iv f1 t )
+
+   idem-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → f ≡ f1
+   idem-<l> refl = refl
+
+   idem-<r> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → g ≡ g1
+   idem-<r> refl = refl
 
    idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
    idem-eval (id a) = refl
@@ -60,26 +67,28 @@
    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 g h)) with eval (iv g h) | idem-eval (iv g h)
+   idem-eval (iv f (iv g h)) with eval (iv g h) | idem-eval (iv g h) 
    idem-eval (iv f (iv g h)) | id a | m = refl
    idem-eval (iv f (iv g h)) | ○ a | m = refl
-   idem-eval (iv π (iv g h)) | < t , t₁ > | m = {!!}
-   idem-eval (iv π' (iv g h)) | < t , t₁ > | m = {!!}
+   idem-eval (iv π (iv g h)) | < t , t₁ > | m = idem-<l> m 
+   idem-eval (iv π' (iv g h)) | < t , t₁ > | m = idem-<r> m
    idem-eval (iv ε (iv g h)) | < t , t₁ > | m = cong ( λ k → iv ε k ) m
    idem-eval (iv (f *) (iv g h)) | < t , t₁ > | m = cong ( λ k → iv (f *) k ) m
-   idem-eval (iv f (iv g h)) | iv f₁ t | m = {!!}
+   idem-eval (iv f (iv g h)) | iv f1 t | m = lemma where
+       lemma :  eval (iv f (iv f1 t)) ≡ iv f (iv f1 t)
+       lemma = ?
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
-   id a ・ g = eval g
+   id a ・ g = g
    ○ a ・ g = ○ _
    < f , g > ・  h = <  f ・ h  ,  g ・ h  >
-   iv f (id _) ・ h = iv f (eval h)
+   iv f (id _) ・ h = iv f h
    iv π < g , g₁ > ・  h = g ・ h
    iv π' < g , g₁ > ・  h = g₁ ・ h
    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 (eval y)
+   iv x y ・ id a = iv x y
    iv f (iv f₁ g) ・ h = iv f (  iv f₁ g ・ h )
 
    _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
@@ -100,7 +109,8 @@
    identityR {a} {b} {iv {a} {b} {.(b ∧ _)} π (iv g h)} |  record {eq = refl } | < t , t₁ > = {!!}
    identityR {a} {b} {iv {a} {b} {.(b ∧ _)} π (iv g h)} |  record {eq = refl } | iv f t = {!!}
    identityR {a} {b} {iv {c} {d} {e} π' (iv g h)} = {!!}
-   identityR {a} {b} {iv {c} {d} {e} f (iv g h)} = {!!}
+   identityR {a} {b} {iv {c} {d} {e} f (iv g h)} with identityR {_} {_} {iv g h}
+   ... | t = {!!}
 
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
    ==←≡ eq = cong (λ k → eval k ) eq
@@ -123,7 +133,7 @@
                identityL : {A B : Objs} {f : Arrows A B} → (id B ・ f) == f
                identityL {_} {_} {id a} = refl
                identityL {_} {_} {○ a} = refl
-               identityL {a} {b} {< f , f₁ >} = {!!}
+               identityL {a} {b} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityL {_} {_} {f}) (identityL {_} {_} {f₁})
                identityL {_} {_} {iv f f₁} = {!!}
                associative : {a b c d : Objs} (f : Arrows c d) (g : Arrows b c) (h : Arrows a b) →
                             (f ・ (g ・ h)) == ((f ・ g) ・ h)