--- a/CCCGraph1.agda	Tue Apr 07 14:33:54 2020 +0900
+++ b/CCCGraph1.agda	Tue Apr 07 15:58:43 2020 +0900
@@ -51,11 +51,16 @@
    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 : {a b c : Objs} → Arrows a ( b ∧ c) → Arrows a b
    pi (id .(_ ∧ _)) = iv π (id _)
    pi < x , x₁ > = x
    pi (iv f x) =  iv π (iv f x)
 
+   pi' : {a b c : Objs} → Arrows a ( b ∧ c) → Arrows a c
+   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
 
@@ -115,10 +120,13 @@
    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-∧ (iv f f1) g h t with eval ( iv f f1) | inspect eval (iv f f1 )
+   std-∧ (iv π < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f1 g h ee
+   std-∧ (iv π' < f1 , f2 >) g h refl | iv π < g , h > | record { eq = ee } = std-∧ f2 g h ee
+   std-∧ (iv π (iv f f1)) g h refl | iv π < g , h > | record { eq = ee } = ?
+   std-∧ (iv x (iv f f1)) g h refl | iv π < g , h > | record { eq = ee } = {!!}  where
+      lemma : ¬ (  eval (iv x (iv f f1)) ≡ iv π < g , h > )
+      lemma ee = {!!}
 
    std-∧' : { a b c : Objs } ( f : Arrows a c ) ( g : Arrows a b ) ( h : Arrows a c ) →  ¬ ( eval f ≡  iv π' < g , h > ) 
    std-∧' = {!!}