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

changeset 1104:81b859b678a8

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 Thu, 29 Dec 2022 14:42:28 +0900
parents 8df83228d148
children fabcb7d9f50c
files src/OPair.agda src/Topology.agda
diffstat 2 files changed, 45 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/OPair.agda	Thu Dec 29 10:58:42 2022 +0900
+++ b/src/OPair.agda	Thu Dec 29 14:42:28 2022 +0900
@@ -194,7 +194,7 @@
 
 ZFP  : (A B : HOD) → HOD
 ZFP  A B = record { od = record { def = λ x → ZFProduct A B x  } 
-        ; odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px } 
+        ; odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px }  -- this is too large
    where
        lemma : (y : Ordinal) → ZFProduct A B y → y o< omax (next (odmax A)) (next (odmax B))
        lemma p ( ab-pair {x} {y} ax by ) with trio< (& A) (& B) 
@@ -212,6 +212,21 @@
 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) 
 
+zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
+zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a
+
+zp1 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef A (zπ1 zx)
+zp1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = aa
+
+zπ2 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
+zπ2 (ab-pair {a} {b} aa bb) = b
+
+zp2 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef B (zπ2 zx)
+zp2 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = bb
+
+zp-iso :  { A B : HOD } → {x : Ordinal } → (p : odef (ZFP A B) x ) → & < * (zπ1 p) , * (zπ2 p) > ≡ x
+zp-iso {A} {B} {_} (ab-pair {a} {b} aa bb)  = refl
+
 ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
 ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
 
--- a/src/Topology.agda	Thu Dec 29 10:58:42 2022 +0900
+++ b/src/Topology.agda	Thu Dec 29 14:42:28 2022 +0900
@@ -65,13 +65,6 @@
    g∩ : {x y : HOD} → genTop P x → genTop P y → genTop P (x ∩ y)
    g∪ : {Q x : HOD} → Q ⊆ P → genTop P (Union Q)
 
--- Limit point
-
-record LP { L : HOD}  (top : Topology L) ( S x : HOD ) (S⊆PL :  S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
-   field
-      neip   : {y : HOD} → OS top ∋ y → y ∋ x → HOD
-      isNeip : {y : HOD} → (o∋y : OS top ∋ y ) → (y∋x : y ∋ x ) → ¬ ( x ≡ neip o∋y y∋x) ∧ ( y ∋ neip o∋y y∋x )
-       
 -- Finite Intersection Property
 
 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
@@ -166,9 +159,35 @@
 
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (TP Top⊗ TQ)
 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (TP Top⊗ TQ) (UFLP→FIP (TP Top⊗ TQ) uflp ) where
-    uflp : {L : HOD} (LP : L ⊆ Power (ZFP P Q)) (F : Filter LP)
-            (uf : ultra-filter {L} {_} {LP} F) → UFLP (TP Top⊗ TQ) LP F uf
-    uflp {L} LP F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? }
+    uflp : {L : HOD} (LPQ : L ⊆ Power (ZFP P Q)) (F : Filter LPQ)
+            (uf : ultra-filter {L} {_} {LPQ} F) → UFLP (TP Top⊗ TQ) LPQ F uf
+    uflp {L} LPQ F uf = record { limit = ? ; P∋limit = ? ; is-limit = ? } where
+         lprod : {x y : Ordinal } → (ly : odef L y) → odef (ZFP P Q) x
+         lprod {x} {y} ly = LPQ ly x ?
+         -- LP : HOD  
+         -- LP = Replace' L ( λ x lx → Replace' x ( λ z xz → * ( zπ1 (LPQ lx (& z) (subst (λ k → odef k (& z)) (sym *iso) xz )))) )
+         LP : HOD  
+         LP = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→P ly ) }
+          ; odmax = & P ; <odmax = ? }   where
+            L→P : {y : Ordinal } → odef L y → HOD
+            L→P {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ1 (LPQ ly z yz )  ≡ x } 
+               ; odmax = & P ; <odmax = ? }
+         LPP : LP ⊆ Power P
+         LPP = ?
+         FP : Filter LPP
+         FP = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? }
+         uFP : ultra-filter FP
+         uFP = record { proper = ? ; ultra = ? }
+         LQ : HOD  
+         LQ = record { od = record { def = λ x → {y z : Ordinal } → (ly : odef L y) → x ≡ & ( L→Q ly ) }
+          ; odmax = & P ; <odmax = ? }   where
+            L→Q : {y : Ordinal } → odef L y → HOD
+            L→Q {y} ly = record { od = record { def = λ x → {z : Ordinal } → (yz : odef (* y) z) → zπ2 (LPQ ly z yz )  ≡ x } 
+               ; odmax = & Q ; <odmax = ? }
+         LQQ : LQ ⊆ Power Q
+         LQQ = ?
+         uflpp : UFLP {P} TP {LP} LPP FP uFP
+         uflpp = ?