--- a/src/Polynominal.agda	Mon Apr 19 23:12:17 2021 +0900
+++ b/src/Polynominal.agda	Tue Apr 20 15:59:28 2021 +0900
@@ -54,6 +54,12 @@
   toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
   toφ {a} {⊤} {b} {c} x∈a z = i
 
+  -- arrow in A[x], equality in A[x] should be a modulo x, that is  k x phi ≈ k x phi'
+  -- the smallest equivalence relation
+  --
+  -- if we use equality on f as in A, Poly is ovioously Hom c b of a Category.
+  -- it is better to define A[x] as an extension of A as described before
+
   record Poly (a c b : Obj A )  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
        x :  Hom A １ a
@@ -66,6 +72,7 @@
   --  For every polynominal ψ(x) : b → c in an indeterminate x : 1 → a over a cartesian or cartesian closed
   --  category A there is a unique arrow f : a ∧ b → c in A such that f ∙ < x ∙ ○ b , id1 A b > ≈ ψ(x).
   --
+  --  equality assumption in uniq should be modulo-x, k x phi ≈ k x phi'
 
   record Functional-completeness {a b c : Obj A} ( p : Poly a c b ) : Set  (c₁ ⊔ c₂ ⊔ ℓ) where
     x = Poly.x p
@@ -81,7 +88,7 @@
     field
       sl :  Hom A a b 
     g :  Hom A １ (b <= a) 
-    g  = (A [ A [ A [ sl o  π ] o < id1 A _ ,  ○ a > ] o π' ]  ) *
+    g  = (A [ sl  o π' ]  ) *
     field
       isSelect : A [  A [ ε  o < g  , Poly.x φ  > ]  ≈  Poly.f φ  ]
       isUnique : (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , Poly.x φ  > ]  ≈  Poly.f φ  ]
@@ -89,8 +96,10 @@
 
   π-cong = IsCCC.π-cong isCCC
   *-cong = IsCCC.*-cong isCCC
+  distr-* = IsCCC.distr-* isCCC
   e2 = IsCCC.e2 isCCC
 
+  -- proof in p.59 Lambek
   functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p 
   functional-completeness {a} {b} {c} p = record {
          fun = k (Poly.x p) (Poly.phi p)
@@ -152,7 +161,7 @@
         --
         --   f ∙ <  x ∙ ○ b  , id1 A b >  ≈ f →  f ≈ k x (phi p)
         -- 
-        -- why  k x {x ∙ ○ b} (iv ii i ) ≡  k x {x ∙ ○ b} i?
+        -- why  k x {x ∙ ○ b} (iv ii i ) ≡  k x {x ∙ ○ b} i?  Lambek p.60
         --   if A is locally small, it is ≡-cong.
         postulate
            k-cong : {a b c : Obj A}  → (x :  Hom A １ a) → (f g :  Hom A b c ) → A [ f ≈ g ] →  (fp : φ x {b} {c} f ) (gp :   φ x {b} {c} g )
@@ -177,9 +186,11 @@
   FC {a} {b} φ = record {
      sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ ,  ○ a  > ] 
      ; isSelect = begin
-        ε ∙ <  (( ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ π ) ∙ < id1 A a , ○ a > ) ∙ π')  * ,  Poly.x φ  > ≈↑⟨ cdr (π-cong (*-cong (car assoc))  refl-hom) ⟩
-        ε ∙ < (((k (Poly.x φ) (Poly.phi φ) ∙ < id1  A _ , ○ a >) ∙ (π ∙ (< id1  A _ , ○ a >))) ∙ π' ) * , Poly.x φ > ≈⟨ {!!} ⟩
-        ε ∙ <  ( (k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ (id1 A _ ∙ π' ) )  * ,  Poly.x φ  > ≈⟨ {!!} ⟩
+        ε ∙ <  ((k (Poly.x φ) (Poly.phi φ)∙ < id1 A _ ,  ○ a > ) ∙ π')  * ,  Poly.x φ  > ≈⟨ {!!} ⟩
+        ε ∙ <  (k (Poly.x φ) (Poly.phi φ)∙ (< id1 A _ ,  ○ a >  ∙ π'))  * ,  Poly.x φ  > ≈⟨ {!!} ⟩
+        ε ∙ ( < (k (Poly.x φ ) (Poly.phi φ) * ) ∙   (Poly.x φ  ∙  ○ １)   ,  id1 A １ > ) ≈⟨ {!!} ⟩ 
+        ε ∙ ( < (k (Poly.x φ ) (Poly.phi φ) * ) ∙ (π  ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ > ) ,  id1 A １ > ) ≈⟨ {!!} ⟩ 
+        ε ∙ ( < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ > , π' ∙  <  Poly.x φ  ∙  ○ １  , id1 A １ >  > ) ≈⟨ {!!} ⟩ 
         ε ∙ ( < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' >   ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ > ) ≈⟨ assoc ⟩ 
         (ε ∙ < ((k (Poly.x φ ) (Poly.phi φ) * ) ∙ π ) , π' >  ) ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ > ≈⟨ car ( IsCCC.e4a isCCC ) ⟩ 
         k (Poly.x φ ) (Poly.phi φ) ∙ <  Poly.x φ  ∙  ○ １  , id1 A １ >  ≈⟨ fc0 φ  ⟩