--- a/CCCGraph1.agda	Sun Apr 05 17:23:58 2020 +0900
+++ b/CCCGraph1.agda	Sun Apr 05 17:57:55 2020 +0900
@@ -99,19 +99,15 @@
    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
-
+   std-iv x y (iv z f) ne with eval (iv z f) 
+   std-iv x y (iv z f) ne | id a = refl
+   std-iv x y (iv z f) ne | ○ a = refl
+   std-iv x y (iv z f) ne | < t , t₁ > = ⊥-elim (ne refl)
+   std-iv (arrow x) _ (iv z f) ne | iv z1 t = refl
+   std-iv π y (iv z f) ne | iv z1 t = refl
+   std-iv π' y (iv z f) ne | iv z1 t = refl
+   std-iv ε y (iv z f) ne | iv z1 t = refl
+   std-iv (x *) y (iv z f) ne | iv z1 t = refl
 
    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