# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1618737101 -32400
# Node ID 65df341f09375dc3cd4f0354ed44e2a35b9e61bd
# Parent  2871dd5b5e63146fdf7556a85f38bac7ff34558c
...

diff -r 2871dd5b5e63 -r 65df341f0937 src/Polynominal.agda
--- a/src/Polynominal.agda	Sun Apr 18 11:19:15 2021 +0900
+++ b/src/Polynominal.agda	Sun Apr 18 18:11:41 2021 +0900
@@ -54,10 +54,11 @@
   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
 
-  record XHom {a ⊤ : Obj A }  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+  record XHom (a b c ⊤ : 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
+       xhom :  Hom A ⊤ a
+       fhom : Hom A b c 
+       phi  :  φ xhom {b} {c} fhom 
 
   record PHom {a ⊤ : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
@@ -81,25 +82,24 @@
          → A [ f  ≈ fun p ]
 
   -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
-  record Fc {a b : Obj A } ( φ : (x : Hom A １ a  ) → XHom {b} {１} )
+  record Fc {a b : Obj A } ( φ :  XHom a １ b １) 
          :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
       sl :  Hom A a b 
-    g : Hom A １ (b <= a) 
-    g = (A [ A [ A [ sl o π ] o < id1 A _ ,  ○ a > ] o π' ]  ) *
+    g :  Hom A １ (b <= a) 
+    g  = (A [ A [ A [ sl o  π ] o < id1 A _ ,  ○ a > ] o π' ]  ) *
     field
-      isSelect : (x : Hom A １ a  ) → A [  A [ ε  o < g , x > ]  ≈  XHom.xhom ( φ x ) ]
-      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , x > ]  ≈   XHom.xhom ( φ x ) ]
-        →  A [ g  ≈ f ]
+      isSelect : A [  A [ ε  o < g  , XHom.xhom φ  > ]  ≈  XHom.fhom φ  ]
+      isUnique : (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , XHom.xhom φ  > ]  ≈   XHom.fhom φ  ]
+        →  A [ g   ≈ f ]
 
   -- functional completeness
-  FC : {a b : Obj A}  → (φ  : Hom A １ a   → XHom {b} {１} )  → Fc φ 
+  FC : {a b : Obj A}  → (φ  : XHom a １ b １ )  → Fc {a} {b} φ 
   FC {a} {b} φ = record {
-     sl = {!!}
+     sl = {!!} -- XHom.fhom φ ? -- A [ k (XHom.fhom φ {!!} ) {!!} o < {!!} , id1 A _  > ] -- (XHom.phi φ x) o {!!} ]
      ; isSelect = {!!} 
      ; isUnique = {!!} 
     } 
-       -- sl = (A [ A [  {!!}  o < id1 A _ ,  ○ a > ] o π' ]  ) *
 
   π-cong = IsCCC.π-cong isCCC
   e2 = IsCCC.e2 isCCC
diff -r 2871dd5b5e63 -r 65df341f0937 src/ToposIL.agda
--- a/src/ToposIL.agda	Sun Apr 18 11:19:15 2021 +0900
+++ b/src/ToposIL.agda	Sun Apr 18 18:11:41 2021 +0900
@@ -33,7 +33,7 @@
          _==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω
          _∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω
          -- { x ∈ a | φ x } : P a
-         select : {a : Obj A} → ( φ : (x : Hom A １ a  ) → XHom {Ω} {１} ) → Hom A １ (P a)
+         select : {a : Obj A} → ( φ :  XHom {!!} {!!} {!!}  ) → Hom A １ (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
      _|-_  :  (List (Hom A １ Ω)) → (p : Hom A １ Ω ) → Set ℓ
      [] |-  p = A [ p ≈  ⊤ ] 
@@ -59,7 +59,7 @@
 
   -- functional completeness
   FC1 : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
-  FC1 = {a b : Obj A}  ( φ : (x : Hom A １ a  ) → XHom {b} {１} ) → Fc φ
+  FC1 = {a b : Obj A}  ( φ : XHom {!!} {!!} {!!} ) → Fc φ
 
   topos→logic : (t : Topos A c ) → ToposNat A １ → FC1  → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a)
   topos→logic t n fc = record {