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

diff -r 28df99fe81de -r 2871dd5b5e63 src/Polynominal.agda
--- a/src/Polynominal.agda	Sun Apr 18 11:00:21 2021 +0900
+++ b/src/Polynominal.agda	Sun Apr 18 11:19:15 2021 +0900
@@ -66,34 +66,6 @@
 
   open PHom
 
-  -- A is A[x] 
-  Polynominal :  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Category c₁ (c₁ ⊔ c₂ ⊔ ℓ) ℓ 
-  Polynominal {a} {⊤} x =  record {
-            Obj  = Obj A;
-            Hom = λ b c → PHom {a} {⊤} {x} b c ;
-            _o_ =  λ{a} {b} {c} x y → record { hom =  hom x ∙ hom y  ; phi = iv (phi x) (phi y) } ;
-            _≈_ =  λ x y → A [ hom x ≈ hom y ] ;
-            Id  =  λ{a} → record { hom = id1 A a ; phi = i } ;
-            isCategory  = record {
-                    isEquivalence =  record { sym = sym-hom ; trans = trans-hom ; refl = refl-hom } ;
-                    identityL  = λ {a b f} → idL ;
-                    identityR  = λ {a b f} → idR ;
-                    o-resp-≈  = λ {a b c f g h i} → resp ;
-                    associative  = λ{a b c d f g h } → assoc 
-               }
-           }  
-
-  Hx :  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) → Functor A (Polynominal x)
-  Hx {a} x = record {
-     FObj = λ a → a
-   ; FMap = λ f → record { hom = f ; phi = i }
-   ; isFunctor = record {
-        identity = refl-hom
-      ; distr = refl-hom
-      ; ≈-cong = λ eq → eq
-     }
-   } 
-
   --
   --  Proposition 6.1
   --
@@ -109,14 +81,6 @@
          → A [ f  ≈ fun p ]
 
   -- 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 [ ε  o < sl , x > ]  ≈  φ x ]
-      isUnique : (x : Hom A １ a  ) → (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , x > ]  ≈  φ x ]
-        →  A [ sl  ≈ f ]
-
   record Fc {a b : Obj A } ( φ : (x : Hom A １ a  ) → XHom {b} {１} )
          :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
diff -r 28df99fe81de -r 2871dd5b5e63 src/ToposIL.agda
--- a/src/ToposIL.agda	Sun Apr 18 11:00:21 2021 +0900
+++ b/src/ToposIL.agda	Sun Apr 18 11:19:15 2021 +0900
@@ -14,19 +14,7 @@
   open Functor
   open import Category.Sets hiding (_o_)
   open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
-
-  data  φ  {a ⊤ : Obj A } ( x : Hom A ⊤ a ) : {b c : Obj A } → Hom A b c → Set ( c₁  ⊔  c₂ ⊔ ℓ) where
-     i   : {b c : Obj A} {k : Hom A b c } → φ x k   
-     ii  : φ x {⊤} {a} x
-     iii : {b c' c'' : Obj A } { f : Hom A b c' } { g : Hom A b c'' } (ψ : φ x f ) (χ : φ x g ) → φ x {b} {c'  ∧ c''} < f , g > 
-     iv  : {b c d : Obj A } { f : Hom A d c } { g : Hom A b d } (ψ : φ x f ) (χ : φ x g ) → φ x (A [ f o g  ] )
-     v   : {b c' c'' : Obj A } { f : Hom A (b ∧ c') c'' }  (ψ : φ x f )  → φ x {b} {c'' <= c'} ( f * )
-     φ-cong   : {b c : Obj A} {k k' : Hom A b c } → A [ k ≈ k' ] → φ x k  → φ x k'
-
-  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
+  open import Polynominal A c
 
   -- record IsLogic    (c : CCC A) 
   --        (Ω : Obj A)
@@ -69,22 +57,11 @@
 
   -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
 
-  record Fc {a b : Obj A } ( φ : (x : Hom A １ a  ) → XHom {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 π' ]  ) *
-    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 ]
+  -- functional completeness
+  FC1 : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
+  FC1 = {a b : Obj A}  ( φ : (x : Hom A １ a  ) → XHom {b} {１} ) → Fc φ
 
-  -- functional completeness
-  FC : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
-  FC = {a b : Obj A}  ( φ : (x : Hom A １ a  ) → XHom {b} {１} ) → Fc φ
-
-  topos→logic : (t : Topos A c ) → ToposNat A １ → FC  → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a)
+  topos→logic : (t : Topos A c ) → ToposNat A １ → FC1  → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a)
   topos→logic t n fc = record {
          _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > (δmono t n ) o < f , g > ]
       ;  _∈_ = λ {a} x α →  A [ ε o < α , x > ]