# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1618705300 -32400
# Node ID cc7103f643b7916faf23b8e3d637be6d5fa103df
# Parent  60b24b3dc0c64823bf275bc15712d587f2dca8a8
...

diff -r 60b24b3dc0c6 -r cc7103f643b7 src/Polynominal.agda
--- a/src/Polynominal.agda	Sat Apr 10 11:39:46 2021 +0900
+++ b/src/Polynominal.agda	Sun Apr 18 09:21:40 2021 +0900
@@ -175,9 +175,35 @@
       uniq : {b c : Obj A} →  (p : PHom b c)  → (f : Hom A (a ∧ b) c) → A [ f ∙ < x ∙ ○ b   , id1 A b  >  ≈ hom p ] 
          → A [ f  ≈ fun p ]
 
+  record XHom {a ⊤ : Obj A }  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+    field
+       xhom : Hom A ⊤ a 
+       phi : {b c : Obj A} → {f : Hom A b c} → φ xhom {b} {c} f
+
+  -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
+  record Select  {a b : Obj A} (Ω : Obj A) ( φ : (x :  Hom A １ a ) → Hom A １ b )
+         :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+    field
+      sl :  Hom A １ (b <= a) 
+      isSelect : (x : Hom A １ a  ) → A [  A [ ε C  o < sl , x > ]  ≈  φ x ]
+      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε C o < f , x > ]  ≈  φ x ]
+        →  A [ sl  ≈ f ]
+
+  φ→Phom : {a b : Obj A} (Ω : Obj A) ( φ : (x :  Hom A １ a ) → Hom A １ b ) → Hom A a b
+  φ→Phom = {!!}
+  
+
+  -- functional completeness
+  FC : {a b : Obj A}  ( φ : (x :  Hom A １ a ) → Hom A １ b ) → Select b φ
+  FC {a} {b} φ = record {
+       sl = (A [ A [ {!!} o < id1 A _ ,  ○ a > ] o π' ]  ) *
+     ; isSelect = {!!} 
+     ; isUnique = {!!} 
+    }
+
   π-cong = IsCCC.π-cong isCCC
   e2 = IsCCC.e2 isCCC
-  {-# TERMINATING #-}
+  -- {-# TERMINATING #-}
   functional-completeness : {a : Obj A} ( x : Hom A １ a ) → Functional-completeness  x 
   functional-completeness {a} x = record {
          fun = λ y → k x (phi y)
@@ -254,11 +280,17 @@
               f ∙  < π , π' >  ≈⟨ cdr (IsCCC.π-id isCCC) ⟩
               f ∙  id1 A _ ≈⟨ idR ⟩
               f ∎  ) where
-          -- fc1 may be wrong. is should be a field of PHom, and  k x {x ∙ ○ b} i may be proved standalone.
           fc1 : {b c : Obj A} (p : PHom b c) → A [ k x (phi p)  ≈ k x {hom p} i ]    -- it looks like (*) in page 60
-          fc1 {b} {c} p = uniq record { hom =  hom p ; phi = i }  ( k x (phi p)) ( begin -- non terminating because of the record, which we may avoid
-               k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈⟨ fc0 p ⟩
-               hom p ∎  )
+          fc1 {b} {c} p with phi p
+          ... | i = refl-hom
+          ... | ii = {!!}  -- it doesn't look good
+          ... | iii t t₁ = {!!}
+          ... | iv t t₁ = {!!}
+          ... | v t = {!!}
+          ... | φ-cong x t = {!!}
+          -- fc1 {b} {c} p = uniq record { hom =  hom p ; phi = i }  ( k x (phi p)) ( begin -- non terminating because of the record, which we may avoid
+          --      k x (phi p) ∙ < x ∙ ○ b , id1 A b > ≈⟨ fc0 p ⟩
+          --      hom p ∎  )
         
 
 -- end