--- a/src/Polynominal.agda	Sun May 16 07:32:31 2021 +0900
+++ b/src/Polynominal.agda	Sun May 16 13:17:22 2021 +0900
@@ -163,7 +163,7 @@
   functional-completeness {a} {b} {c} p = record {
          fun = k (Poly.x p) (Poly.phi p)
        ; fp = fc0 (Poly.x p) (Poly.f p) (Poly.phi p)
-       ; uniq = λ f eq  → uniq   (Poly.x p) (Poly.f p) (Poly.phi p)  f (Poly.nf p ) eq
+       ; uniq = λ f eq  → uniq (Poly.x p) (Poly.f p) (Poly.phi p)  f (Poly.nf p ) eq
      } where 
         fc0 : {a b c : Obj A}  → (x :  Hom A １ a) (f :  Hom A b c) (phi  :  φ x {b} {c} f )
            → A [  k x phi ∙ <  x ∙ ○ b  , id1 A b >  ≈ f ]
@@ -226,20 +226,28 @@
                k x phi ≈↑⟨ ki x f phi ne ⟩
                k x {f} (i _) ≈↑⟨ car fx=p ⟩
                k x {f' ∙ < x ∙ ○ b , id1 A b >} (i _)  ≈⟨ trans-hom (sym assoc)  (cdr (IsCCC.distr-π isCCC) ) ⟩ -- ( f' ∙ < x ∙ ○ b , id1 A b> ) ∙ π'
-               f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii (i _)  (i _)  ) -- ( f' ∙ < (x ∙ ○ b) ∙ π'              , id1 A b ∙ π' > ) 
-                  ≈⟨ cdr (begin 
-                   k x (iii (i (x ∙ ○ b)) (i (id1 A _))) ≈⟨⟩
-                   < ( x ∙ (○ b)) ∙ π' , id1 A _ ∙  π' > ≈⟨ π-cong {!!}  refl-hom  ⟩
-                   <  π , id1 A _ ∙  π' > ≈↑⟨ π-cong (IsCCC.e3a isCCC) refl-hom ⟩
-                   <  π ∙  < π , (○ b) ∙ π' > , id1 A _ ∙  π' > ≈⟨⟩
-                   < k x (iv ii (i (○ b))) , k x (i (id1 A _)) > ∎ ) ⟩
-               f' ∙ < k x {x ∙ ○ b} (iv ii (i _)  ) , k x {id1 A b} (i _)  >   ≈⟨ refl-hom ⟩
+               f' ∙ k x {< x ∙ ○ b , id1 A b >} (iii (i _)  (i _)  ) ≈⟨⟩                         -- ( f' ∙ < (x ∙ ○ b) ∙ π'  , id1 A b ∙ π' > ) 
+               f' ∙ <  k x (i (x ∙ ○ b)) ,  k x {id1 A b} (i _) >  ≈⟨ cdr (π-cong u2 refl-hom) ⟩ -- ( f' ∙ < (x ∙ ○ b) ∙ π' , id1 A b ∙ π' > ) 
                f' ∙ < k x {x} ii ∙ < π , k x {○ b} (i _)  >  , k x {id1 A b} (i _)  >   -- ( f' ∙ < π ∙ < π , (x ∙ ○ b) ∙ π' >  , id1 A b ∙ π' > ) 
                    ≈⟨ cdr (π-cong (cdr (π-cong refl-hom (car e2))) idL ) ⟩ 
                f' ∙  <  π ∙ < π , (○ b ∙ π' ) >  , π' >   ≈⟨ cdr (π-cong (IsCCC.e3a isCCC)  refl-hom) ⟩
                f' ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
                f' ∙  id1 A _ ≈⟨ idR ⟩
-               f' ∎  ) 
+               f' ∎  )  where
+                   u1 : x ∙ ○ b ≈ ( x  ∙ ○ _ ) ∙ ( < π , k x {○ b} (i _) >  ∙ < x ∙ ○ b , id1 A b > )
+                   u1 = begin
+                     x ∙ ○ b ≈↑⟨ cdr e2 ⟩
+                     x ∙ ( ○ _ ∙ _ )  ≈⟨ assoc ⟩
+                     ( x  ∙ ○ _ ) ∙ ( < π , k x {○ b} (i _) >  ∙ < x ∙ ○ b , id1 A b > )  ∎  
+                   u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) > 
+                   u2 = begin
+                     k x {x ∙ ○ b} (i _) ≈↑⟨ assoc ⟩     --- (x ∙ ○ b) ∙ π'
+                     x ∙ (○ _ ∙ π') ≈⟨ cdr e2 ⟩
+                     x ∙ ○ _ ≈↑⟨ IsCCC.e3a isCCC ⟩
+                     k x {x} ii ∙ < ( x ∙ ○ _ )  ,  k x {○ b} (i _) >  ≈⟨ {!!} ⟩
+                     k x {x} ii ∙ < π ∙ < x ∙ {!!} , id1 A _ >  ,  k x {○ b} (i _) >  ≈⟨ {!!} ⟩
+                     k x {x} ii ∙ < π ∙ id1 A _  ,  k x {○ b} (i _) >  ≈⟨ {!!} ⟩
+                     k x {x} ii ∙ < π ,             k x {○ b} (i _) > ∎  
 
 
   -- functional completeness ε form