--- a/src/CCC.agda	Sun Feb 11 11:25:40 2024 +0900
+++ b/src/CCC.agda	Tue Jul 02 08:34:33 2024 +0900
@@ -285,6 +285,14 @@
      Monik : {a : Obj A} (h : Hom A a Ω)  → Mono A (equalizer (Ker h))
      Monik h = record { isMono = λ f g → monic (Ker h ) } 
 
+--  Nat as iniitla object (1→ ℕ → ℕ)
+--
+--     0     s
+--  1 -→  ℕ --→ ℕ 
+--  |     |h    |h
+--  + --→ A --→ A  
+--     a     f
+
 record NatD {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)  ( １ : Obj A) : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
          Nat   : Obj A

--- a/src/Polynominal.agda	Sun Feb 11 11:25:40 2024 +0900
+++ b/src/Polynominal.agda	Tue Jul 02 08:34:33 2024 +0900
@@ -87,11 +87,14 @@
   pid : {a : Obj A} (x : Hom A １ a) → (c : Obj A)  → Polym x c c
   pid {a} x c = record { f = id1 A c ; phi = i (id1 A c) }
 
+  pf : {a : Obj A} (x : Hom A １ a) → {b c : Obj A}  → (f : Hom A b c)  → Polym x b c
+  pf {a} x f = record { f = f ; phi = i f }
+
   pcomp : {a : Obj A} (x : Hom A １ a) { b c d : Obj A } ( f : Polym x c d ) → (g : Polym x b c) → Polym x b d
   pcomp {a} x {b} {c} {d} f g = record { f = Polym.f f ∙ Polym.f g  ; phi = iv (i (Polym.f f)) (i (Polym.f g)) } 
 
   data P≈ {a : Obj A} (x : Hom A １ a) : { b c : Obj A } ( f g : Polym x b c ) → Set ( c₁  ⊔  c₂ ⊔ ℓ) where
-     p-refl : { b c  : Obj A}  {f : Polym x b c } → P≈ x f f
+     p-refl : { b c  : Obj A}  {f g : Polym x b c } → A [ Polym.f f ≈ Polym.f g ]  → P≈ x f g
      p-sym : { b c  : Obj A}  {f g : Polym x b c } → P≈ x f g → P≈ x g f
      p-trans : { b c : Obj A} {χ ψ φ  : Polym x b c} → P≈ x χ ψ → P≈ x ψ φ → P≈ x χ φ 
      p-comp : { b c d : Obj A} {g : Polym x c d } {f : Polym x b c } {h : Polym x b d} 
@@ -103,6 +106,8 @@
      p-idl : { c d : Obj A} {ψ  : Polym x c d } → P≈ x  (pcomp x (pid x _) ψ) ψ
      p-assoc : { b c d e : Obj A} (χ  : Polym x d e) (ψ  : Polym x c d ) (φ  : Polym x b c )
          → P≈ x (pcomp x χ (pcomp x ψ φ ) ) (pcomp x (pcomp x χ ψ) φ ) 
+     -- p-<> : { b c d e : Obj A} {g : Polym x c d } {f : Polym x c e} {h : Polym x c (e ∧ d)} → 
+     --    A [ < Polym.f f , Polym.f g > ≈ Polym.f h ] → P≈ x ? h
 
 
   PolyC : {a : Obj A} (x : Hom A １ a) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) (c₁ ⊔ c₂ ⊔ ℓ) 
@@ -113,7 +118,7 @@
      _≈_ =  λ f g → P≈ x f g ;
      Id  =  λ{b} → pid x b ;
      isCategory  = record {
-        isEquivalence =  record {refl = p-refl ; trans = p-trans ; sym = p-sym  } ;
+        isEquivalence =  record {refl = p-refl refl-hom  ; trans = p-trans ; sym = p-sym  } ;
         identityL  = p-idl ;
         identityR  = p-idr ;
         o-resp-≈  = p-resp  ;
@@ -121,6 +126,31 @@
      }
    } 
 
+  PolyCCC : {a : Obj A} (x : Hom A １ a) → CCC (PolyC x)
+  PolyCCC {a} x = record {
+     １ = １ ;
+     ○ = λ b → pf x (○ b)  ; 
+     _∧_ = _∧_ ; 
+     <_,_> = λ f g → pf x ( < Polym.f f , Polym.f g > ) ;
+     π = pf x π ; 
+     π' = pf x π' ; 
+     _<=_ = _<=_ ; 
+     _* = λ f → pf x ( (Polym.f f) *  ) ; 
+     ε = pf x ε ; 
+     isCCC  = record {
+       e2 = p-refl (IsCCC.e2 isCCC ) ;
+       e3a = ? ;
+       e3b = ? ;
+       e3c = ? ;
+       π-cong = ? ;
+       -- closed
+       e4a = ? ;
+       e4b = ? ;
+       *-cong = ? 
+      }
+    }
+
+
 
   -- an assuption needed in k x phi ≈ k x phi'
   --   k x (i x) ≈ k x ii
@@ -148,6 +178,13 @@
       uniq : ( f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b , id1 A b > ≈ Poly.f p ]
          → A [ f ≈ fun  ]
 
+  record P-Functional-completeness {a : Obj A} (x : Hom A １ a) {b c : Obj A} ( p : Polym x b c ) : Set  (c₁ ⊔ c₂ ⊔ ℓ) where
+    field
+      fun  : Hom A (a ∧ b) c
+      fp   : P≈ x (pf x ( fun ∙ <  x ∙ ○ b   , id1 A b  >))  p
+      uniq : ( f : Hom A (a ∧ b) c) → P≈ x (pf x ( f ∙ < x ∙ ○ b , id1 A b >)) p 
+         → A [ f ≈ fun  ]
+
   -- ε form
   -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x
   record Fc {a b : Obj A } ( φ :  Poly a b １ )
@@ -210,6 +247,14 @@
   --  Instead of replacing x in Poly.phi ψ, we can use simple application with this fuctional completeness
   --  in the internal language of Topos.
   --
+
+  p-functional-completeness : {a : Obj A} (x : Hom A １ a) { b c : Obj A} ( p : Polym x b c ) → P-Functional-completeness x p
+  p-functional-completeness {a} x {b} {c} p = record {
+         fun = k x (Polym.phi p)
+       ; fp = ? -- fc0 x (Polym.f p) (Polym.phi p)
+       ; uniq = ? -- λ f eq  → uniq x (Polym.f p) (Polym.phi p)  f eq
+     } 
+
   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)