--- a/CCCGraph1.agda	Wed Apr 08 16:02:21 2020 +0900
+++ b/CCCGraph1.agda	Wed Apr 08 17:34:19 2020 +0900
@@ -105,13 +105,7 @@
    open import Data.Empty 
    open import Relation.Nullary 
 
-   open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
-
-   isnot-∧ : (a : Objs) → Dec ( {x y : Objs } → ¬ a ≡ (x ∧ y ) )
-   isnot-∧ (atom x) = yes ( λ {x} {y} () )
-   isnot-∧ ⊤ = yes ( λ {x} {y} () )
-   isnot-∧ (a ∧ b) =  no ( λ ne → ⊥-elim ( ne {a} {b} refl ))
-   isnot-∧ (b <= a) = yes ( λ {x} {y} () )
+   open import Relation.Binary.HeterogeneousEquality as HE using (_≅_;refl)
 
    std-iv : {a b c d : Objs} (x : Arrow c d) (y : Arrow b c ) (f : Arrows a b) 
         →  ( {b1 b2 : Objs } → {g : Arrows a b1 } {h : Arrows a b2 } → ¬ (eval f) ≅ < g , h > )
@@ -155,7 +149,16 @@
    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 f₁ g)) = ?
+   idem-eval (iv f (iv g h)) with eval (iv g h) | idem-eval (iv g h) | inspect 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 | _ = refl-<l> m
+   idem-eval (iv π' (iv g h)) | < t , t₁ > | m | _ = refl-<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 | record { eq = ee } = trans lemma (cong ( λ k → iv f k ) m )  where
+      lemma : eval (iv f (iv f₁ t)) ≡ iv f (eval (iv f₁ t))
+      lemma =  std-iv f f₁ t {!!}
 
    assoc-iv : {a b c d : Objs} (x : Arrow c d) (f : Arrows b c) (g : Arrows a b ) → eval (iv x (f ・ g)) ≡ eval (iv x f ・ g)
    assoc-iv x (id a) g = {!!}