--- a/src/Polynominal.agda	Wed May 12 11:30:41 2021 +0900
+++ b/src/Polynominal.agda	Wed May 12 12:52:54 2021 +0900
@@ -54,6 +54,8 @@
   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
 
+  -- The Polynominal arrow  -- λ term in A
+  --
   -- 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
   --
@@ -64,10 +66,10 @@
 
   record Poly (a c b : Obj A )  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
-       x :  Hom A １ a
+       x :  Hom A １ a                                            -- λ x
        f :  Hom A b c
-       phi  :  φ x {b} {c} f 
-       idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a  ≈ id1 A a
+       phi  :  φ x {b} {c} f                                      -- construction of f
+       idx : {a : Obj A} → {x : Hom A １ a} → x ∙ ○ a  ≈ id1 A a  -- minimum equivalence
 
   -- since we have A[x] now, we can proceed the proof on p.64 in some possible future
 
@@ -128,46 +130,37 @@
                (x ∙ ○ a ) ∙ π   ≈⟨ car (Poly.idx p) ⟩
                id1 A a ∙ π   ≈⟨ idL ⟩
                k x ii  ∎  
-  ki p x .(< f₁  , f₂ > ) (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin
+  ki p x _ (iii {_} {_} {_} {f₁}{ f₂} fp₁ fp₂ ) = begin
                < f₁ ,  f₂  > ∙ π'  ≈⟨ IsCCC.distr-π isCCC ⟩
                < f₁ ∙ π'  ,  f₂   ∙ π' >  ≈⟨ π-cong (ki p x f₁ fp₁) (ki p x f₂ fp₂) ⟩
                 k x (iii  fp₁ fp₂ )  ∎  
-  ki p x .((A Category.o _) _) (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin
+  ki p x _ (iv {_} {_} {_} {f₁} {f₂} fp fp₁) = begin
                (f₁ ∙ f₂  ) ∙ π'  ≈↑⟨ assoc ⟩
                f₁  ∙ ( f₂ ∙ π')  ≈↑⟨ cdr (IsCCC.e3b isCCC) ⟩
                f₁  ∙ ( π'  ∙ < π , (f₂ ∙ π' )  >)  ≈⟨ assoc ⟩
                (f₁  ∙ π' ) ∙ < π , (f₂ ∙ π' )  >  ≈⟨ resp (π-cong refl-hom (ki p x _ fp₁) ) (ki p x _ fp) ⟩
                k x fp ∙ < π , k x fp₁ >  ≈⟨⟩
                k x (iv fp fp₁ )  ∎  
-  ki p x .((C CCC.*) _) (v fp) = {!!}
-  ki p x f (φ-cong x₁ fp) = {!!}
+  ki p x _ (v {_} {_} {_} {f} fp) = begin
+               (f *) ∙ π' ≈⟨ distr-*  ⟩
+               ( f ∙ < π' ∙ π , π'  > ) * ≈↑⟨ *-cong (cdr (IsCCC.e3b isCCC)) ⟩
+               ( f ∙ ( π'  ∙  < π ∙ π , < π' ∙  π , π' > > ) ) *  ≈⟨ *-cong assoc  ⟩
+               ( (f ∙ π')  ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨ *-cong ( car ( ki p x _ fp)) ⟩
+               ( k x fp ∙  < π ∙ π , < π' ∙  π , π' > > ) *  ≈⟨⟩
+               k x (v fp )  ∎  
+  ki p x f (φ-cong {_} {_} {f₁} {f} eq fp) = begin
+               f ∙ π' ≈↑⟨ car eq ⟩
+               f₁ ∙ π' ≈⟨ ki p x _ fp ⟩
+               k x fp  ≈⟨⟩
+               k x (φ-cong eq  fp )  ∎  
   k-cong : {a b c : Obj A}  → (f g :  Poly a c b )
         → Poly.x f ≡ Poly.x g 
         → A [ Poly.f f ≈ Poly.f g ] → A [ k (Poly.x f) (Poly.phi f)   ≈ k (Poly.x g) (Poly.phi g) ]
-  k-cong {a} {b} {c} f g refl f=f = kcong f (Poly.x f ) (Poly.f f) (Poly.f g) f=f ( Poly.phi f ) ( Poly.phi g) where
-     kcong : {a b b' c c' : Obj A} → Poly a c' b'
-        → (x : Hom A １ a) → (f g : Hom A b c ) → (f=g : f ≈ g ) → (fp  :  φ x {b} {c} f )( gp :  φ x {b} {c} g ) → A [ k x fp  ≈ k x gp ]
-     kcong {a} {b} {c} p x f g f=g i i = resp refl-hom f=g
-     kcong {a} {.(CCC.１ C)} {_} {.a} p x f .x f=g i ii = begin
-          k x {f} i ≈⟨⟩
-          f ∙ π' ≈⟨ car f=g ⟩
-          x ∙ π' ≈⟨ ki p x x ii ⟩
-          k x ii ∎   
-     kcong {a} {b} {_} {.((C CCC.∧ _) _)} p x f .(< g₁ , g₂ >)  f=g i (iii {_} {_} {_} {g₁} {g₂} gp₁ gp₂) = begin
-          k x i ≈⟨ car f=g ⟩
-          < g₁ , g₂ > ∙ π' ≈⟨ IsCCC.distr-π isCCC ⟩
-          < g₁ ∙ π' , g₂ ∙ π' >  ≈⟨ IsCCC.π-cong isCCC (ki p x _ gp₁ ) (ki p x _ gp₂) ⟩
-          < k x gp₁  , k x gp₂  >  ≈⟨⟩
-          k x (iii gp₁ gp₂) ∎   
-     kcong {a} {b} {_} {c} p x f .((A Category.o _) _) f=g i (iv gp gp₁) = {!!}
-     kcong {a} {b} {_} {.((C CCC.<= _) _)} p x f .((C CCC.*) _) f=g i (v gp) = {!!}
-     kcong {a} {b} {_} {c} p x f g f=g i (φ-cong x₁ gp) = {!!}
-     kcong {a} {.(CCC.１ C)} {_} {.a} p x .x g f=g ii gp = {!!}
-     kcong {a} {b} {_} {.((C CCC.∧ _) _)} p x .(CCC.< C , _ > _) g f=g (iii fp fp₁) gp = {!!}
-     kcong {a} {b} {_} {c} p x .((A Category.o _) _) g f=g (iv fp fp₁) gp = {!!}
-     kcong {a} {b} {_} {.((C CCC.<= _) _)} p x .((C CCC.*) _) g f=g (v fp) gp = {!!}
-     kcong {a} {b} {_} {c} p x f g f=g (φ-cong x₁ fp) gp = {!!}
-
+  k-cong {a} {b} {c} f g refl f=f = begin
+          k (Poly.x f) (Poly.phi f) ≈↑⟨ ki f (Poly.x f)  _ (Poly.phi f) ⟩
+          Poly.f f ∙ π' ≈⟨ car f=f  ⟩
+          Poly.f g ∙ π'  ≈⟨  ki f (Poly.x f)  _ (Poly.phi g) ⟩
+          k (Poly.x g) (Poly.phi g) ∎   
 
   -- proof in p.59 Lambek
   functional-completeness : {a b c : Obj A} ( p : Poly a c b ) → Functional-completeness p