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

changeset 1137:d618788852e5

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 Fri, 13 Jan 2023 09:30:31 +0900
parents 181ffd308ab5
children dd18bb8d2893
files src/filter.agda
diffstat 1 files changed, 23 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/src/filter.agda	Fri Jan 13 08:22:20 2023 +0900
+++ b/src/filter.agda	Fri Jan 13 09:30:31 2023 +0900
@@ -323,9 +323,30 @@
       FX : HOD
       FX = F⊆X {L} {P} LP F
       FX∋F : odef FX (& (filter F))
-      FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = ? ; filter2 = ? ; proper = ? }  , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ 
+      oF = & (filter F)
+      mf11 : { p q : Ordinal } → odef L q → odef (* oF) p →  (* p) ⊆ (* q)  → odef (* oF) q
+      mf11 {p} {q} Lq Fp p⊆q = subst₂ (λ j k → odef j k ) (sym *iso) &iso ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) 
+             (subst₂ (λ j k → odef j k ) *iso (sym &iso)  Fp) p⊆q )
+      mf12 : { p q : Ordinal } → odef (* oF)  p →  odef (* oF) q  → odef L (& ((* p) ∩ (* q))) → odef (* oF) (& ((* p) ∩ (* q)))
+      mf12 {p} {q} Fp Fq Lpq = subst (λ k → odef k (& ((* p) ∩ (* q))) ) (sym *iso) 
+        ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso)  Fp) (subst₂ (λ j k → odef j k ) *iso (sym &iso)  Fq) Lpq)
+      FX∋F = ⟪ record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) (f⊆L F) ; filter1 = mf11 ; filter2 = mf12 
+        ; proper = subst₂ (λ j k →  ¬ (odef j k) ) (sym *iso) ord-od∅ Fprop  }  
+          , subst (λ k → filter F ⊆ k ) (sym *iso) ( λ x → x ) ⟫ 
       SUP⊆ : (B : HOD) → B ⊆ FX → IsTotalOrderSet B → SUP FX B
-      SUP⊆ B B⊆FX OB = record { sup = Union B ; isSUP = record { ax = ? ; x≤sup = ?  } }
+      SUP⊆ B B⊆FX OB = record { sup = Union B ; isSUP = record { ax = mf13 ; x≤sup = ?  } } where
+          mf16 : Union B ⊆ L
+          mf16 record { owner = b ; ao = Bb ; ox = bx } = is-filter.f⊆L ( proj1 ( B⊆FX Bb )) bx
+          mf17 : {p q : Ordinal} → odef L q → odef (* (& (Union B))) p → * p ⊆ * q → odef (* (& (Union B))) q
+          mf17 {p} {q} Lq bp p⊆q with subst (λ k → odef k p ) *iso bp
+          ... | record { owner = owner ; ao = ao ; ox = ox } = subst (λ k → odef k q) (sym *iso) 
+                record { owner = ? ; ao = ? ; ox = ? } 
+          mf14 : is-filter LP (& (Union B)) 
+          mf14 = record { f⊆L = subst (λ k → k ⊆ L) (sym *iso) mf16 ; filter1 = mf17 ; filter2 = ? ; proper = ? } 
+          mf15 :  filter F ⊆ Union B
+          mf15 {x} Fx = record { owner = ? ; ao = ? ; ox = subst (λ k → odef k x) (sym *iso) Fx  } 
+          mf13 : odef FX (& (Union B))
+          mf13 = ⟪ mf14  , subst (λ k → filter F ⊆ k ) (sym *iso) mf15  ⟫
       mx : Maximal  FX
       mx = Zorn-lemma (∈∅< FX∋F) SUP⊆  
       imf : is-filter {L} {P} LP (& (Maximal.maximal mx))