Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1215:881e85e12e38

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Mar 2023 14:46:53 +0900
parents 93e1869bb57c
children 6861b48c1e08
files src/Tychonoff.agda
diffstat 1 files changed, 13 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Sun Mar 05 13:41:57 2023 +0900
+++ b/src/Tychonoff.agda	Sun Mar 05 14:46:53 2023 +0900
@@ -341,6 +341,13 @@
          F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy)
          FPSet : HOD
          FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))
+         FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋  ZFP q Q → FPSet ∋ q
+         FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = ? ; x=ψz = ? } where
+             ty04 : q ≡ Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq ) xy)))
+             ty04 = ==→o≡ record { eq→ = ? ; eq← = ? } where
+                ty041 : {x : Ordinal} → odef q x → odef (Replace' (* (& (ZFP q Q)))
+                  (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy)))) x
+                ty041 {x} qx = record { z = _ ; az = subst (λ k → odef k (& < * x , * ? > )) (sym *iso) (ab-pair qx ? )  ;  x=ψz = ? }
          FPSet⊆PP :  FPSet  ⊆ Power P
          FPSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw
          ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } 
@@ -349,7 +356,8 @@
          FP : Filter {Power P} {P} (λ x → x)
          FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = {!!} } where
              ty01 : {p q : HOD} → Power P ∋ q → FPSet ∋ p → p ⊆ q → FPSet ∋ q
-             ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = record { z = _ ; az = ty02 ; x=ψz = cong (&) ty04 }  where
+             ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FPSet∋zpq q⊆P (ty10 ty05 ty06 )
+                where
                   --  p ≡ (Replace' (* x) (λ y xy → (zπ1 (F⊆pxq (subst (odef (filter.Filter.filter F)) (sym &iso) fx) xy))
                   --  x = ( px , qx )  , px ⊆ q
                   ty03 : Power (ZFP P Q) ∋ ZFP q Q
@@ -358,6 +366,8 @@
                   p⊆P {w} pw with subst (λ k → odef k w) (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψz))  pw
                   ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) 
                        (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) (subst (λ k → odef (* x) k) (sym &iso) az1 ))  )
+                  q⊆P : q ⊆ P
+                  q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw )
                   x⊆pxq : * x ⊆ ZFP p Q
                   x⊆pxq {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
                   ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
@@ -370,11 +380,8 @@
                   ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fx) x⊆pxq
                   ty06 : ZFP p Q ⊆ ZFP q Q
                   ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
-                  ty02 : filter F ∋  ZFP q Q
-                  ty02 = filter1 F ty03 ty05 ty06
-                  ty04 : q ≡ Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 
-                       (F⊆pxq (subst (odef (filter F)) (sym &iso) ty02) xy)))
-                  ty04 = ?
+                  ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋  ZFP q Q
+                  ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq
 
          UFP : ultra-filter FP
          UFP = record { proper = {!!} ; ultra = {!!} }