Mercurial > hg > Members > kono > Proof > category
view src/ToposIL.agda @ 1065:5a9f5a4cadaa
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 27 Apr 2021 05:10:29 +0900 |
parents | a17348c201e5 |
children | f8b0f1b6fe84 |
line wrap: on
line source
open import CCC open import Level open import Category open import cat-utility open import HomReasoning open import Data.List hiding ( [_] ) module ToposIL {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (c : CCC A) where open Topos open Equalizer -- open ≈-Reasoning A hiding (_∙_) open CCC.CCC c open Functor open import Category.Sets hiding (_o_) open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym) open import Polynominal A c record IsLogic (Ω : Obj A) (⊤ : Hom A 1 Ω) (P : Obj A → Obj A) (_==_ : {a : Obj A} (x y : Hom A 1 a ) → Hom A 1 Ω) (_∈_ : {a : Obj A} (x : Hom A 1 a ) (α : Hom A 1 (P a) ) → Hom A 1 Ω) (select : {a : Obj A} → ( φ : Poly a Ω 1 ) → Hom A 1 (P a)) (apply : {a : Obj A} (p : Poly a Ω 1 ) → ( x : Hom A 1 a ) → Poly a Ω 1 ) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field isSelect : {a : Obj A} → ( φ : Poly a Ω 1 ) → {c : Obj A} (h : Hom A c 1 ) → A [ ( ( Poly.x φ ∈ select φ ) == Poly.f φ ) ∙ h ≈ ⊤ ∙ ○ c ] uniqueSelect : {a : Obj A} → ( φ : Poly a Ω 1 ) → (α : Hom A 1 (P a) ) → {c : Obj A} (h : Hom A c 1 ) → A [ ( Poly.f φ == ( Poly.x φ ∈ α ) ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ ( select φ == α ) ∙ h ≈ ⊤ ∙ ○ c ] isApply : {a : Obj A} (x y : Hom A 1 a ) → (q p : Poly a Ω 1 ) → {c : Obj A} (h : Hom A c 1 ) → A [ ( x == y ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f (apply p x ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f (apply p y ) ∙ h ≈ ⊤ ∙ ○ c ] applyCong : {a : Obj A} (x : Hom A 1 a ) → (q p : Poly a Ω 1 ) → {c : Obj A} (h : Hom A c 1 ) → ( A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] ) → ( A [ Poly.f (apply q x ) ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f (apply p x ) ∙ h ≈ ⊤ ∙ ○ c ] ) record InternalLanguage (Ω : Obj A) (⊤ : Hom A 1 Ω) (P : Obj A → Obj A) : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) where field _==_ : {a : Obj A} (x y : Hom A 1 a ) → Hom A 1 Ω _∈_ : {a : Obj A} (x : Hom A 1 a ) (α : Hom A 1 (P a) ) → Hom A 1 Ω -- { x ∈ a | φ x } : P a select : {a : Obj A} → ( φ : Poly a Ω 1 ) → Hom A 1 (P a) apply : {a : Obj A} (p : Poly a Ω 1 ) → ( x : Hom A 1 a ) → Poly a Ω 1 isIL : IsLogic Ω ⊤ P _==_ _∈_ select apply _⊢_ : {a : Obj A} (p : Poly a Ω 1 ) (q : Poly a Ω 1 ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) _⊢_ {a} p q = {c : Obj A} (h : Hom A c 1 ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] _,_⊢_ : {a : Obj A} (p : Poly a Ω 1 ) (p1 : Poly a Ω 1 ) (q : Poly a Ω 1 ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) _,_⊢_ {a} p p1 q = {c : Obj A} (h : Hom A c 1 ) → A [ Poly.f p ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f p1 ∙ h ≈ ⊤ ∙ ○ c ] → A [ Poly.f q ∙ h ≈ ⊤ ∙ ○ c ] expr : {a b c : Obj A} (p : Hom A 1 Ω ) → ( x : Hom A 1 a ) → Poly a Ω 1 expr p x = record { x = x ; f = p ; phi = i } ⊨_ : (p : Hom A 1 Ω ) → Set ( c₁ ⊔ c₂ ⊔ ℓ ) ⊨ p = {c : Obj A} (h : Hom A c 1 ) → A [ p ∙ h ≈ ⊤ ∙ ○ c ] -- ○ b -- b -----------→ 1 -- | | -- m | | ⊤ -- ↓ char m ↓ -- a -----------→ Ω -- (n : ToposNat A 1) -- open NatD -- open ToposNat n -- N : Obj A -- N = Nat iNat open import ToposEx A c using ( δmono ) -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) → f ∙ x ≈ φ x -- functional completeness FC0 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) FC0 = {a : Obj A} (t : Topos A c) ( φ : Poly a (Ω t)1) → Functional-completeness φ FC1 : Set ( suc c₁ ⊔ suc c₂ ⊔ suc ℓ ) FC1 = {a : Obj A} (t : Topos A c) ( φ : Poly a (Ω t)1) → Fc φ topos→logic : (t : Topos A c ) → ToposNat A 1 → FC0 → FC1 → InternalLanguage (Topos.Ω t) (Topos.⊤ t) (λ a → (Topos.Ω t) <= a) topos→logic t n fc0 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 > ] -- { x ∈ a | φ x } : P a ; select = λ {a} φ → Fc.g ( fc t φ ) ; apply = λ {a} φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙ ○ _ , id1 A _ > ; phi = i } ; isIL = record { isSelect = {!!} ; uniqueSelect = {!!} ; isApply = {!!} ; applyCong = {!!} } } module IL1 (Ω : Obj A) (⊤ : Hom A 1 Ω) (P : Obj A → Obj A) (il : InternalLanguage Ω ⊤ P) where open InternalLanguage il il00 : {a : Obj A} (p : Poly a Ω 1 ) → p ⊢ p il00 {a} p h eq = eq il01 : {a : Obj A} (p : Poly a Ω 1 ) (q : Poly a Ω 1 ) → p ⊢ q → q ⊢ p → A [ Poly.f p ≈ Poly.f q ] il01 {a} p q p<q q<p = {!!} il011 : {a : Obj A} (p q q1 : Poly a Ω 1 ) → q ⊢ p → q , q1 ⊢ p il011 {a} p q q1 p<q h tq tq1 = p<q h tq il012 : {a : Obj A} (p q r : Poly a Ω 1 ) → q ⊢ p → q , p ⊢ r → q ⊢ r il012 {a} p q r p<q pq<r h qt = pq<r h qt (p<q h qt) il02 : {a : Obj A} (x : Hom A 1 a ) → ⊨ (x == x) il02 = {!!} --- (b : Hom A 1 a) → φ y ⊢ φ' y → φ b ⊢ φ' b il03 : {a : Obj A} (b : Hom A 1 a ) → (q p : Poly a Ω 1 ) → q ⊢ p → apply q b ⊢ apply p b il03 {a} b q p q<p h = IsLogic.applyCong (InternalLanguage.isIL il ) b q p h (q<p h) --- a == b → φ a ⊢ φ b il04 : {a : Obj A} (x y : Hom A 1 a ) → (q p : Poly a Ω 1 ) → ⊨ (x == y) → q ⊢ apply p x → q ⊢ apply p y il04 {a} x y q p eq q<px h qt = IsLogic.isApply (InternalLanguage.isIL il ) x y q p h (eq h) qt (q<px h qt ) --- ⊨ x ∈ select φ == φ x il05 : {a : Obj A} → (q : Poly a Ω 1 ) → ⊨ ( ( Poly.x q ∈ select q ) == Poly.f q ) il05 {a} = IsLogic.isSelect (InternalLanguage.isIL il ) --- q ⊢ φ x == x ∈ α --- ----------------------- --- q ⊢ select φ == α --- il06 : {a : Obj A} → (q : Poly a Ω 1 ) → (α : Hom A 1 (P a) ) → ⊨ ( Poly.f q == ( Poly.x q ∈ α ) ) → ⊨ ( select q == α ) il06 {a} q p eq h = IsLogic.uniqueSelect (InternalLanguage.isIL il ) q p h (eq h)