--- a/CCCGraph1.agda	Sat Apr 04 17:51:01 2020 +0900
+++ b/CCCGraph1.agda	Sat Apr 04 19:24:14 2020 +0900
@@ -36,12 +36,29 @@
    eval (id a) = id a
    eval (○ a) = ○ a
    eval < f , f₁ > = < eval f , eval f₁ >
-   eval (iv π < f , g > ) =  eval f
-   eval (iv π' < f , g > ) = eval g
-   eval (iv f g) = iv f (eval g)
+   eval (iv f g) with eval g
+   eval (iv f g) | id a = iv f (id a)
+   eval (iv f g) | ○ a = iv f ( ○ a )
+   eval (iv π g) | < h , i > = h
+   eval (iv π' g) | < h , i > = i
+   eval (iv f g) | < h , i > = iv f < h , i >
+   eval (iv f g) | iv h i = iv f ( iv h i )
+
+   idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
+   idem-eval (id a) = refl
+   idem-eval (○ a) = refl
+   idem-eval < f , f₁ > = cong₂ ( λ j k → < j , k > ) (idem-eval f) (idem-eval f₁)
+   idem-eval (iv f g) with eval g
+   idem-eval (iv f g) | id a = refl
+   idem-eval (iv f g) | ○ a = refl
+   idem-eval (iv π g) | < h , i > = {!!}
+   idem-eval (iv π' g) | < h , i > = {!!}
+   idem-eval (iv f g) | < h , i > = {!!}
+   idem-eval (iv f g) | iv f₁ t = {!!}
 
    _・_ :  {a b c : Objs } (f : Arrows b c ) → (g : Arrows a b) → Arrows a c
    id a ・ g = eval g
+   ○ a ・ g = ○ _
    < f , g > ・  h = <  f ・ h  ,  g ・ h  >
    iv f (id _) ・ h = iv f (eval h)
    iv π < g , g₁ > ・  h = g ・ h
@@ -51,7 +68,6 @@
    iv f ( (○ a)) ・ g = iv f ( ○ _ )
    iv x y ・ id a = iv x (eval y)
    iv f (iv f₁ g) ・ h = iv f (  iv f₁ g ・ h )
-   ○ a ・ g = ○ _
 
    _==_  : {a b : Objs } → ( x y : Arrows a b ) → Set (c₁ ⊔ c₂)
    _==_ {a} {b} x y   = eval x  ≡ eval  y 
@@ -62,11 +78,16 @@
    identityR {a} {.(_ ∧ _)} {< f , f₁ >} = cong₂ (λ j k → < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
    identityR {a} {b} {iv f (id a)} = refl
    identityR {a} {b} {iv f (○ a)} = refl
-   identityR {a} {b} {iv π < g , g₁ >} = {!!}
-   identityR {a} {b} {iv π' < g , g₁ >} = {!!}
+   identityR {a} {b} {iv π < g , g₁ >} = identityR {_} {_} {g} 
+   identityR {a} {b} {iv π' < g , g₁ >} = identityR {_} {_} {g₁} 
    identityR {a} {b} {iv ε < f , f₁ >} = cong₂ (λ j k → iv ε < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
    identityR {a} {_} {iv (x *) < f , f₁ >} = cong₂ (λ j k → iv (x *) < j , k > ) (identityR {_} {_} {f} ) (identityR  {_} {_} {f₁})
-   identityR {a} {b} {iv f (iv g h)} = {!!}
+   identityR {a} {b} {iv {c} {d} {e} π (iv g h)} with inspect eval (iv g h) | eval (iv g h)
+   identityR {.(b ∧ _)} {b} {iv {.(b ∧ _)} {b} {.(b ∧ _)} π (iv g h)} | record {eq = refl } | id .(b ∧ _) = refl
+   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)} = {!!}
 
    ==←≡ : {A B : Objs} {f g : Arrows A B} → f ≡ g → f == g
    ==←≡ eq = cong (λ k → eval k ) eq