--- a/CCCGraph1.agda	Wed Apr 08 17:34:19 2020 +0900
+++ b/CCCGraph1.agda	Wed Apr 08 17:48:24 2020 +0900
@@ -156,9 +156,10 @@
    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 {!!}
+   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 = {!!}