# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1617928170 -32400
# Node ID a929a58a389d611f2ac29abddcfde186f83e0da6
# Parent  c3e6fddb04e8cca65aea51bd279634f76ef19120
fix depenency in internal language

diff -r c3e6fddb04e8 -r a929a58a389d src/ToposIL.agda
--- a/src/ToposIL.agda	Fri Apr 09 09:05:59 2021 +0900
+++ b/src/ToposIL.agda	Fri Apr 09 09:29:30 2021 +0900
@@ -4,7 +4,7 @@
 open import cat-utility
 open import HomReasoning
 open import Data.List hiding ( [_] )
-module ToposIL   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) (t : Topos A c ) (n : ToposNat A (CCC.１ c)) where
+module ToposIL   {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A)   where
 
   open Topos
   open Equalizer
@@ -26,18 +26,16 @@
   --    field
   --        a : {!!}
 
-  record Logic :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+  record InternalLanguage (Ω : Obj A) (⊤ : Hom A (CCC.１ c) Ω) (P  : Obj A → Obj A)
+          :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
      field
-         Ω : Obj A
-         ⊤ : Hom A (CCC.１ c) Ω
-         P  : Obj A → Obj A
          _==_ : {a : Obj A} (x y : Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) Ω
          _∈_ : {a : Obj A} (x :  Hom A  (CCC.１ c) a ) (α : Hom A (CCC.１ c) (P a) ) → Hom A (CCC.１ c) Ω
          -- { x ∈ a | φ x } : P a
          select : {a b : Obj A}  (α : Hom A (CCC.１ c) (P a) ) → ( (x :  Hom A  (CCC.１ c) a ) →  Hom A (CCC.１ c) Ω ) → Hom A (CCC.１ c) (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
-     _|-_  : {a : Obj A} (p : Hom A (CCC.１ c) (Ω t )) → Set ℓ
-     _|-_  {a} p = A [ p ≈  Topos.⊤ t ] 
+     _|-_  : {a : Obj A} (p : Hom A (CCC.１ c) Ω ) → Set ℓ
+     _|-_  {a} p = A [ p ≈  ⊤ ] 
   
 --             ○ b
 --       b -----------→ 1
@@ -46,16 +44,17 @@
 --       ↓    char m    ↓
 --       a -----------→ Ω
 
-  open NatD
-  open ToposNat n
+  -- (n : ToposNat A (CCC.１ c))
+  -- open NatD
+  -- open ToposNat n
 
-  N : Obj A
-  N = Nat iNat 
+  -- N : Obj A
+  -- N = Nat iNat 
 
-  open import ToposEx A c t n using ( δmono  )
+  open import ToposEx A c using ( δmono  )
 
   -- λ (x ∈ a) → φ x
-  record Select  {a b : Obj A}  (α : Hom A (CCC.１ c) ((Topos.Ω t) <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b )
+  record Select  {a b : Obj A} (Ω : Obj A) (α : Hom A (CCC.１ c) (Ω <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b )
          :  Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
     field
       sl :  Hom A (CCC.１ c) (b <= a) 
@@ -63,14 +62,11 @@
 
   -- functional completeness
   FC : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
-  FC = {a b : Obj A}  (α : Hom A (CCC.１ c) ((Topos.Ω t) <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b ) → Select α φ
+  FC = {a b : Obj A}  (α : Hom A (CCC.１ c) (b <= a) ) ( φ : (x :  Hom A  (CCC.１ c) a ) → Hom A (CCC.１ c) b ) → Select b α φ
 
-  topos→logic : FC  → Logic 
-  topos→logic fc = record {
-         Ω = Topos.Ω t
-      ;  ⊤ = Topos.⊤ t
-      ;  P  = λ a → (Topos.Ω t) <= a
-      ;  _==_ = λ {b} f g →   A [ char t < id1 A b , id1 A b > δmono  o < f , g > ]
+  topos→logic : (t : Topos A c ) → ToposNat A (CCC.１ c)  → FC  → 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 [ CCC.ε c o < α , x > ]
       -- { x ∈ a | φ x } : P a
       ;  select = λ {a} α φ →  Select.sl ( fc α φ )