Mercurial > hg > Members > kono > Proof > category
changeset 1042:a929a58a389d internal-language
fix depenency in internal language
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 09 Apr 2021 09:29:30 +0900 |
| parents | c3e6fddb04e8 |
| children | 35a3d5b194b7 |
| files | src/ToposIL.agda |
| diffstat | 1 files changed, 16 insertions(+), 20 deletions(-) [+] |
line wrap: on
line diff
--- 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 α φ )