Mercurial > hg > Members > kono > Proof > category

changeset 1051:1948ce61e2f0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
... Polynominal arg type
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 18 Apr 2021 20:45:44 +0900
parents 65df341f0937
children 1a237825ea08
files src/Polynominal.agda src/ToposIL.agda
diffstat 2 files changed, 15 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/src/Polynominal.agda	Sun Apr 18 18:11:41 2021 +0900
+++ b/src/Polynominal.agda	Sun Apr 18 20:45:44 2021 +0900
@@ -54,11 +54,11 @@
   toφ : {a ⊤ b c : Obj A } → ( x∈a : Hom A ⊤ a ) → (z : Hom A b c ) → φ {a} x∈a z  
   toφ {a} {⊤} {b} {c} x∈a z = i
 
-  record XHom (a b c ⊤ : Obj A )  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
+  record Poly (a b ⊤ : Obj A )  : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
-       xhom :  Hom A ⊤ a
-       fhom : Hom A b c 
-       phi  :  φ xhom {b} {c} fhom 
+       x :  Hom A ⊤ a
+       f :  Hom A ⊤ b
+       phi  :  φ x {⊤} {b} f 
 
   record PHom {a ⊤ : Obj A } { x : Hom A ⊤ a } (b c : Obj A) : Set (c₁ ⊔ c₂ ⊔ ℓ)  where
     field
@@ -82,21 +82,21 @@
          → A [ f  ≈ fun p ]
 
   -- f ≡ λ (x ∈ a) → φ x , ∃ (f : b <= a) →  f ∙ x ≈  φ x  
-  record Fc {a b : Obj A } ( φ :  XHom a １ b １) 
+  record Fc {a b : Obj A } ( φ :  Poly a 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 : A [  A [ ε  o < g  , XHom.xhom φ  > ]  ≈  XHom.fhom φ  ]
-      isUnique : (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , XHom.xhom φ  > ]  ≈   XHom.fhom φ  ]
+      isSelect : A [  A [ ε  o < g  , Poly.x φ  > ]  ≈  Poly.f φ  ]
+      isUnique : (f : Hom A １ (b <= a) )  → A [  A [ ε o < f , Poly.x φ  > ]  ≈  Poly.f φ  ]
         →  A [ g   ≈ f ]
 
   -- functional completeness
-  FC : {a b : Obj A}  → (φ  : XHom a １ b １ )  → Fc {a} {b} φ 
+  FC : {a b : Obj A}  → (φ  : Poly a b １ )  → Fc {a} {b} φ 
   FC {a} {b} φ = record {
-     sl = {!!} -- XHom.fhom φ ? -- A [ k (XHom.fhom φ {!!} ) {!!} o < {!!} , id1 A _  > ] -- (XHom.phi φ x) o {!!} ]
+     sl = A [ k (Poly.x φ ) (Poly.phi φ) o < id1 A _ ,  ○ a  > ] 
      ; isSelect = {!!} 
      ; isUnique = {!!} 
     } 
--- a/src/ToposIL.agda	Sun Apr 18 18:11:41 2021 +0900
+++ b/src/ToposIL.agda	Sun Apr 18 20:45:44 2021 +0900
@@ -33,11 +33,11 @@
          _==_ : {a : Obj A} (x y : Hom A １ a ) → Hom A １ Ω
          _∈_ : {a : Obj A} (x :  Hom A １ a ) (α : Hom A １ (P a) ) → Hom A １ Ω
          -- { x ∈ a | φ x } : P a
-         select : {a : Obj A} → ( φ :  XHom {!!} {!!} {!!}  ) → Hom A １ (P a)
+         select : {a : Obj A} → ( φ :  Poly a Ω １ ) → Hom A １ (P a)
          -- isTL : IsLogic c Ω ⊤ P _==_ _∈_  _|-_
-     _|-_  :  (List (Hom A １ Ω)) → (p : Hom A １ Ω ) → Set ℓ
-     [] |-  p = A [ p ≈  ⊤ ] 
-     (h ∷ t) |-  p = {!!}
+     -- _|-_  :  (List (Hom A １ Ω)) → (p : Hom A １ Ω ) → Set ℓ
+     -- [] |-  p = A [ p ≈  ⊤ ] 
+     -- (h ∷ t) |-  p = {!!}
   
 --             ○ b
 --       b -----------→ 1
@@ -59,13 +59,13 @@
 
   -- functional completeness
   FC1 : Set ( suc c₁  ⊔  suc c₂ ⊔ suc ℓ )
-  FC1 = {a b : Obj A}  ( φ : XHom {!!} {!!} {!!} ) → Fc φ
+  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 {
          _==_ = λ {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 φ )
+      ;  select = λ {a} φ →  Fc.g ( fc t φ )
       -- ;  isTL = {!!}
     }