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

changeset 1101:7ce2cc622c92

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 Wed, 28 Dec 2022 18:14:29 +0900
parents c90eec304cfa
children a9a7ad7784cc
files src/Topology.agda src/cardinal.agda src/generic-filter.agda src/zorn.agda
diffstat 4 files changed, 41 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/Topology.agda	Mon Dec 26 14:00:57 2022 +0900
+++ b/src/Topology.agda	Wed Dec 28 18:14:29 2022 +0900
@@ -31,6 +31,8 @@
 open ODC O
 
 open import filter
+open import OPair O
+
 
 record Topology  ( L : HOD ) : Set (suc n) where
    field
@@ -38,9 +40,16 @@
        OS⊆PL :  OS ⊆ Power L 
        o∪ : { P : HOD }  →  P  ⊆ OS           → OS ∋ Union P
        o∩ : { p q : HOD } → OS ∋ p →  OS ∋ q  → OS ∋ (p ∩ q)
+-- closed Set
+   CS : HOD
+   CS = record { od = record { def = λ x → odef OS (& ( L ＼ (* x ))) } ; odmax = & L ; <odmax = tp02 } where
+       tp02 : {y : Ordinal } → odef OS (& (L ＼ * y)) → y o< & L
+       tp02 {y} nop = ?
+       -- ∈∅< ( proj1 nop )
 
 open Topology
 
+
 record _covers_ ( P q : HOD  ) : Set (suc n) where
    field
        cover   : {x : HOD} → q ∋ x → HOD
@@ -58,7 +67,7 @@
 
 -- Limit point
 
-record LP ( L S x : HOD ) (top : Topology L) (S⊆PL :  S ⊆ Power L ) ( S∋x : S ∋ x ) : Set (suc n) where
+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 )
@@ -66,38 +75,49 @@
 -- Finite Intersection Property
 
 data Finite-∩ (S : HOD) : HOD → Set (suc n) where
-   fin-∩e : {x : HOD} → S ∋ x → Finite-∩ S x
-   fin-∩  : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
+   fin-e : {x : HOD} → S ∋ x → Finite-∩ S x
+   fin-∩ : {x y : HOD} → Finite-∩ S x → Finite-∩ S y → Finite-∩ S (x ∩ y)
 
-record FIP  ( L P : HOD ) : Set (suc n) where
+record FIP {L : HOD} (top : Topology L)  ( P : HOD ) : Set (suc n) where
    field
-       fipS⊆PL :  P ⊆ Power L 
+       fipS⊆PL :  P ⊆ CS top
        fip≠φ : { x : HOD } → Finite-∩ P x → ¬ ( x ≡ od∅ )
 
 -- Compact
 
 data Finite-∪ (S : HOD) : HOD → Set (suc n) where
-   fin-∪e : {x : HOD} → S ∋ x → Finite-∪ S x
+   fin-e : {x : HOD} → S ∋ x → Finite-∪ S x
    fin-∪  : {x y : HOD} → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (x ∪ y)
 
-record Compact  ( L P : HOD ) : Set (suc n) where
+record Compact  {L : HOD} (top : Topology L) ( P : HOD ) : Set (suc n) where
    field
-       finCover        : {X y : HOD} → X covers P         → P ∋ y →  HOD
-       isFinCover      : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → finCover xp P∋y ∋ y
-       isFininiteCover : {X y : HOD} → (xp : X covers P ) → (P∋y : P ∋ y ) → Finite-∪ X (finCover xp P∋y )
+       finCover        : {X : HOD} → X ⊆ OS top → X covers P → HOD
+       isFinCover      : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → (finCover xo xcp ) covers P
+       isFiniteCover   : {X : HOD} → (xo : X ⊆ OS top) → (xcp : X covers P ) → Finite-∪ X (finCover xo xcp  )
 
 -- FIP is Compact
 
-FIP→Compact : {L P : HOD} → Topology L → FIP L P → Compact L P
-FIP→Compact = {!!}
+FIP→Compact : {L P : HOD} → (top : Topology L ) → FIP top P → Compact top P
+FIP→Compact {L} {P} TL fip = record { finCover = ? ; isFinCover = ? ; isFiniteCover = ? }
 
-Compact→FIP : {L P : HOD} → Topology L → Compact L P → FIP L P
+Compact→FIP : {L P : HOD} → (top : Topology L ) → Compact top P → FIP top P
 Compact→FIP = {!!}
 
 -- Product Topology
 
-_Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology {!!}
-_Top⊗_ = {!!}
+open ZFProduct 
+
+_Top⊗_ : {P Q : HOD} → Topology P → Topology Q → Topology (ZFP P Q)
+_Top⊗_ {P} {Q} TP TQ = record {
+       OS    = POS
+    ;  OS⊆PL = ?
+    ;  o∪ = ?
+    ;  o∩ = ?
+  } where
+      box : HOD
+      box = ZFP (OS TP) (OS TQ) 
+      POS : HOD
+      POS = ?
 
 -- existence of Ultra Filter 
 
--- a/src/cardinal.agda	Mon Dec 26 14:00:57 2022 +0900
+++ b/src/cardinal.agda	Wed Dec 28 18:14:29 2022 +0900
@@ -46,12 +46,12 @@
 -- A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
 
 Func :  OD
-Func = record { def = λ x → def ZFProduct x
+Func = record { def = λ x → def ZFPair x
     ∧ ( (a b c : Ordinal) → odef (* x) (& < * a , * b >) ∧ odef (* x) (& < * a , * c >) →  b ≡  c ) }
 
 FuncP :  ( A B : HOD ) → HOD
 FuncP A B = record { od = record { def = λ x → odef (ZFP A B) x
-    ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 (proj1 p) ≡ pi1 (proj1 q) → pi2 (proj1 p) ≡ pi2 (proj1 q) ) }
+    ∧ ( (x : Ordinal ) (p q : odef (ZFP A B ) x ) → pi1 ? ≡ pi1 ? → pi2 ? ≡ pi2 ? ) }
        ; odmax = odmax (ZFP A B) ; <odmax = λ lt → <odmax (ZFP A B) (proj1 lt) }
 
 record Injection (A B : Ordinal ) : Set n where
--- a/src/generic-filter.agda	Mon Dec 26 14:00:57 2022 +0900
+++ b/src/generic-filter.agda	Wed Dec 28 18:14:29 2022 +0900
@@ -236,7 +236,9 @@
     →  (LP : L ⊆ Power P ) →  (Lp0 : L ∋ p  )
     →  ( {q : HOD} → (Lq : L ∋ q ) → NonAtomic L q Lq )
     →  ¬ ( (ctl-M C) ∋ filter ( genf ( P-GenericFilter P L p LP Lp0  C )) )
-lemma232 P L p C LP Lp0 NA MG = {!!}
+lemma232 P L p C LP Lp0 NA MG = {!!} where
+    D : HOD  -- P - G
+    D = ?
 
 --
 --   val x G = { val y G | ∃ p → G ∋ p → x ∋ < y , p > }
--- a/src/zorn.agda	Mon Dec 26 14:00:57 2022 +0900
+++ b/src/zorn.agda	Wed Dec 28 18:14:29 2022 +0900
@@ -1109,6 +1109,7 @@
      ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
      ... | tri≈ ¬a x=0 ¬c = record { supf = λ _ → MinSUP.sup (ysup f mf ay) ; asupf = MinSUP.as (ysup f mf ay) ; supf-mono = λ _ → o≤-refl 
           ; zo≤sz = zo≤sz ; is-minsup = is-minsup ; cfcs = λ a<b b≤0 → ⊥-elim ( ¬x<0 (subst (λ k → _ o< k ) x=0 (ordtrans<-≤ a<b b≤0)))    } where
+          -- initial case
 
           mf : ≤-monotonic-f A f
           mf x ax = ⟪ case2 mf00 , proj2 (mf< x ax ) ⟫ where