--- a/CCCGraph1.agda	Mon Apr 06 17:48:24 2020 +0900
+++ b/CCCGraph1.agda	Tue Apr 07 14:33:54 2020 +0900
@@ -51,6 +51,11 @@
    eval (iv (f *) (iv g h)) | < t , t₁ > = iv (f *) < t , t₁ > 
    eval (iv f (iv g h)) | iv f1 t = iv f (iv f1 t) 
 
+   pi : {a b c : Objs} → { f : Arrows a b } { g : Arrows a c } → Arrows a ( b ∧ c) → Arrows a b
+   pi (id .(_ ∧ _)) = iv π (id _)
+   pi < x , x₁ > = x
+   pi (iv f x) =  iv π (iv f x)
+
    refl-<l> : {a b c : Objs} → { f f1 : Arrows a b } { g g1 : Arrows a c }  → < f , g > ≡ < f1 , g1 > → f ≡ f1
    refl-<l> refl = refl
 
@@ -109,6 +114,15 @@
    std-iv ε y (iv z f) ne | iv z1 t = refl
    std-iv (x *) y (iv z f) ne | iv z1 t = refl
 
+   std-∧ : { a b c : Objs } ( f : Arrows a b ) ( g : Arrows a b ) ( h : Arrows a c ) →  ¬ ( eval f ≡  iv π < g , h > ) 
+   std-∧ f g h t with eval f | inspect eval f
+   std-∧ {a} {b} {_} (iv π < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f1 g h ee
+   std-∧ {a} {b} {_} (iv π' < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f2 g h ee
+   std-∧ {a} {b} {_} (iv f (iv f₁ f1)) g h refl | iv π < g , h > | record { eq = ee } = {!!}
+
+   std-∧' : { a b c : Objs } ( f : Arrows a c ) ( g : Arrows a b ) ( h : Arrows a c ) →  ¬ ( eval f ≡  iv π' < g , h > ) 
+   std-∧' = {!!}
+
    idem-eval :  {a b : Objs } (f : Arrows a b ) → eval (eval f) ≡ eval f
    idem-eval (id a) = refl
    idem-eval (○ a) = refl
@@ -126,22 +140,11 @@
    idem-eval (iv π' (iv {_} {_} {d} g h)) | < t , t₁ > | m = refl-<r> m
    idem-eval (iv ε (iv {_} {_} {d} g h)) | < t , t₁ > | m = cong ( λ k → iv ε k ) m
    idem-eval (iv (f *) (iv {_} {_} {d} g h)) | < t , t₁ > | m = cong ( λ k → iv (f *) k ) m
-   idem-eval (iv f (iv {a} {c} {d} g h)) | iv {a} {c} {d1} f1 t | m with  isnot-∧ d1 | inspect eval (iv g h) 
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv f1 t | m | yes p | record { eq = ee } = lemma where
-      lemma1 :  eval (iv f ( iv f1 t)) ≡ iv f (eval ( iv f1 t))
-      lemma1 =  std-iv f f1 t p
-      lemma : eval (iv f (  iv f1 t)) ≡ iv f ( iv f1 t)
-      lemma = begin
-            eval (iv f (  iv f1 t))
-         ≡⟨ lemma1 ⟩
-            iv f (eval ( iv f1 t))
-         ≡⟨ cong (λ k → iv f k ) m ⟩
-            iv f ( iv f1 t)
-        ∎  where open ≡-Reasoning
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {atom x} f₁ t | m | no ¬p | record { eq = ee } = ⊥-elim ( ¬p (λ ()) )
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {⊤} f₁ t | m | no ¬p | record { eq = ee } =  ⊥-elim ( ¬p (λ ()) )
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {d1 <= d2} f₁ t | m | no ¬p | record { eq = ee } =  ⊥-elim ( ¬p (λ ()) )
-   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {_} {_} {d1 ∧ d2} f₁ t | m | no ¬p | record { eq = ee } = {!!}
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {atom _} f1 t | m = trans (std-iv f f1 t (λ ()) ) (cong (λ k → iv f k ) m )
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {⊤} f1 t | m = trans (std-iv f f1 t (λ ()) ) (cong (λ k → iv f k ) m )
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {d1 <= d2} f1 t | m =  trans (std-iv f f1 t (λ ()) ) (cong (λ k → iv f k ) m )
+   idem-eval (iv f (iv {_} {_} {d} g h)) | iv {a} {_} {d1 ∧ d2} f1 t | m = {!!}
+   --   lemma : eval (iv f (  iv f1 t)) ≡ iv f ( iv f1 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 = refl