--- a/CCCGraph1.agda	Sun Apr 05 13:00:59 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 17:23:58 2020 +0900
@@ -88,6 +88,31 @@
    open import Data.Empty 
    open import Relation.Nullary 
 
+   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} () )
+
+   std-iv : {a b c d : Objs} (x : Arrow c d) (y : Arrow b c ) (f : Arrows a b) 
+        →  ( {x y : Objs } → ¬ b ≡ ( x ∧ y ) )   → eval (iv x ( iv y f ) ) ≡ iv x ( eval (iv y f ) )
+   std-iv x y (id a) _ = refl
+   std-iv x y (○ a) _ = refl
+   std-iv x y < f , f₁ > ne = ⊥-elim (ne refl)
+   std-iv x y (iv {_} {_} {e} z f) ne with isnot-∧ e
+   ... | no yy = {!!}
+   ... | yes nn with eval (iv y (iv z f)) | inspect eval (iv y (iv z f)) | std-iv y z f nn 
+   ... | t | record { eq = refl } | u = begin
+            eval (iv x (iv y (iv z f)) )
+         ≡⟨ {!!} ⟩
+            iv x (iv y (eval (iv z f)))
+         ≡⟨ sym ( cong ( λ k → iv x k ) u) ⟩
+            iv x (eval (iv y (iv z f)) )
+         ≡⟨⟩
+            iv x t
+         ∎  where open ≡-Reasoning
+
+
    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 = refl
    assoc-iv x (○ a) g = refl