Mercurial > hg > Members > kono > Proof > category

changeset 1064:a17348c201e5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
apply
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Apr 2021 07:08:12 +0900
parents f1f625c3866c
children 5a9f5a4cadaa
files src/ToposIL.agda
diffstat 1 files changed, 52 insertions(+), 43 deletions(-) [+]
line wrap: on
line diff
--- a/src/ToposIL.agda	Sun Apr 25 21:18:48 2021 +0900
+++ b/src/ToposIL.agda	Mon Apr 26 07:08:12 2021 +0900
@@ -16,17 +16,24 @@
   open import Relation.Binary.PropositionalEquality hiding ( [_] ; sym)
   open import Polynominal A c
 
-  -- record IsLogic    (c : CCC A) 
-  --        (Ω : Obj A)
-  --        (⊤ : Hom A １ Ω)
-  --        (P  : Obj A → Obj A)
-  --        (_==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A ( a ∧ a ) Ω)
-  --        (_∈_ : {a : Obj A} (x : Hom A １ a ) → Hom A ( a ∧ P a ) Ω)
-  --        (_|-_  : {a : Obj A} (x : List ( Hom A １ a ) ) → Hom A {!!} Ω)
-  --           :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
-  --    field
-  --        a : {!!}
-
+  record IsLogic (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A)
+         (_==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω)
+         (_∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω)
+         (select : {a : Obj A} → ( φ :  Poly a Ω １ ) → Hom A １ (P a))
+         (apply : {a  : Obj A}  (p : Poly a  Ω １ )  → ( x : Hom A １ a ) →  Poly a  Ω １ )
+             :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
+     field
+         isSelect : {a : Obj A} → ( φ :  Poly a Ω １ ) → {c : Obj A} (h : Hom A c １ )
+            → A [ ( ( Poly.x φ ∈ select φ ) == Poly.f φ )  ∙ h  ≈  ⊤ ∙  ○  c ]
+         uniqueSelect : {a : Obj A} → ( φ :  Poly a Ω １ ) → {c : Obj A} (h : Hom A c １ )
+            → (α : Hom A １ (P a) )
+            → A [ ( ( Poly.x φ ∈ α )  ==  Poly.f φ )  ∙ h  ≈  ⊤ ∙  ○  c ]
+            → A [ ( select φ == α )  ∙ h  ≈  ⊤ ∙  ○  c ]
+         isApply : {a : Obj A}  (x y : Hom A １ a ) → (q p : Poly a  Ω １ ) 
+            → {c : Obj A} (h : Hom A c １ )  → 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 ]  
 
   record InternalLanguage (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A)
           :   Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ ) where
@@ -35,7 +42,8 @@
          _∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω
          -- { x ∈ a | φ x } : P a
          select : {a : Obj A} → ( φ :  Poly a Ω １ ) → Hom A １ (P a)
-         -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
+         apply : {a  : Obj A}  (p : Poly a  Ω １ )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
+         isTL : IsLogic Ω ⊤ P _==_ _∈_  select apply
      _⊢_  : {a : Obj A}  (p : Poly a  Ω １ ) (q : Poly a  Ω １ ) → Set  ( c₁  ⊔  c₂ ⊔ ℓ ) 
      _⊢_  {a}  p q = {c : Obj A} (h : Hom A c １ ) → A [ Poly.f p ∙  h  ≈  ⊤ ∙  ○  c  ]
          → A [   Poly.f q ∙ h  ≈  ⊤ ∙  ○  c  ] 
@@ -45,35 +53,9 @@
          → A [   Poly.f q  ∙ h  ≈  ⊤ ∙  ○  c  ] 
      expr : {a b c  : Obj A}  (p : Hom A １ Ω  )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
      expr p x = record { x = x ;  f = p ; phi = i }
-
-     apply : {a  : Obj A}  (p : Poly a  Ω １ )  → ( x : Hom A １ a ) →  Poly a  Ω １ 
-     apply {a} p x = apply1 Ω (Poly.f p) (Poly.phi p)  where
-        apply1 :  (Ω : Obj A) (f :  Hom A １  Ω) ( phi  :  φ (Poly.x p) {１} { Ω} f ) →  Poly  a  Ω １
-        apply2 :  (Ω : Obj A) (f :  Hom A １  Ω) ( phi  :  φ (Poly.x p) {１} { Ω} f ) →  Poly.x ( apply1 Ω f phi ) ≡ x
-        apply1 _ f i = record { x = x ; f = f ; phi = i }
-        apply1 _ f ii = record { x = x ; f = x ; phi = ii }
-        apply1 .(c ∧ b) f (iii {_} {c} {b} {g} {h} pg ph ) =
-            record { x = x ; f = < Poly.f (apply1 _ g pg)  , Poly.f (apply1 _ h ph) >
-              ; phi = iii (subst (λ k → φ k (Poly.f ag)) (apply2 _ g pg) (Poly.phi ag))   
-               (subst (λ k → φ k (Poly.f ah)) (apply2 _ h ph) (Poly.phi ah)) }  where
-             ag : Poly  a  c １
-             ag = apply1 _ g pg
-             ah : Poly  a  b １
-             ah = apply1 _ h ph
-        apply1 _ .(_ ∙  _) (iv ph ph₁) = {!!}
-        apply1 _ .(_ *) (v ph) = {!!}
-        apply1 _ f (φ-cong x ph) = {!!}
-        apply2 _ f i = refl
-        apply2 _ f ii = refl
-        apply2 _ f (iii ph ph1) = refl
-        apply2 _ f (iv ph ph1 ) = refl
-        apply2 _ f (v ph) = refl
-        apply2 _ f (φ-cong x ph) = refl
-
      ⊨_ :   (p : Hom A １ Ω  ) →  Set  ( c₁  ⊔  c₂ ⊔ ℓ )
      ⊨  p = {c : Obj A} (h : Hom A c １ )  → A [ p  ∙ h  ≈  ⊤ ∙  ○  c ] 
 
-
 --             ○ b
 --       b -----------→ 1
 --       |              |
@@ -93,16 +75,24 @@
   -- 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)１) → Functional-completeness φ
+
   FC1 : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
   FC1 = {a : Obj A}  (t : Topos A c) ( φ : Poly a (Ω t)１) → 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 {
+  topos→logic : (t : Topos A c ) → ToposNat A １ → 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 φ )
-      -- ;  isTL = {!!}
+      ;  apply = λ {a}  φ x → record { x = x ; f = Functional-completeness.fun (fc0 t φ ) ∙ < x ∙  ○ _ , id1 A _ >  ; phi = i }
+      ;  isTL = record {
+           isSelect = {!!}
+         ; uniqueSelect = {!!}
+         ; isApply = {!!}
+        }
     } 
 
   module IL1 (Ω : Obj A) (⊤ : Hom A １ Ω) (P  : Obj A → Obj A) (il : InternalLanguage  Ω ⊤ P) where
@@ -123,12 +113,31 @@
      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 １ a ) → {c : Obj A} (h : Hom A c １ )  → A [ ( x == x )  ∙ h  ≈  ⊤ ∙  ○  c ]
+     il02 : {a : Obj A} (x : Hom A １ a ) → ⊨ (x == x) 
      il02 = {!!}
 
+     --- (b : Hom A １ a) → φ y  ⊢ φ' y  → φ b  ⊢ φ' b
+     il03 : {a : Obj A}  (b : Hom A １ a ) → (q p : Poly a  Ω １ ) 
+        → q ⊢ p → apply q b  ⊢ apply p b
+     il03 {a} = {!!}
+
      --- a == b → φ a  ⊢ φ b
      il04 : {a : Obj A}  (x y : Hom A １ a ) → (q p : Poly a  Ω １ ) 
-        → {c : Obj A} (h : Hom A c １ )  → A [ ( x == y )  ∙ h  ≈  ⊤ ∙  ○  c ] 
+        → ⊨ (x == y) 
         → q ⊢ apply p x → q ⊢ apply p y
      il04 {a} = {!!}
   
+     --- ⊨ x ∈ select φ == φ x
+     il05 : {a : Obj A}  → (q : Poly a  Ω １ ) 
+        → ⊨ ( ( Poly.x q ∈ select q ) == Poly.f q  )
+     il05 {a} = {!!}
+  
+     ---    q ⊢  φ x == x ∈ α 
+     ---   ----------------------- 
+     ---    q ⊢ select φ == α
+     ---
+     il06 : {a : Obj A}  → (q : Poly a  Ω １ )  → (α : Hom A １ (P a) )
+        → ⊨ ( Poly.f q  == ( Poly.x q ∈ α ) ) 
+        → ⊨ ( select q == α )
+     il06 {a} = {!!}
+