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

changeset 1126:3091ac71a999

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 Tue, 10 Jan 2023 03:00:04 +0900
parents edef8810a023
children c4f4868a8cdd
files src/ODUtil.agda src/filter.agda
diffstat 2 files changed, 21 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/ODUtil.agda	Tue Jan 10 02:19:08 2023 +0900
+++ b/src/ODUtil.agda	Tue Jan 10 03:00:04 2023 +0900
@@ -71,6 +71,9 @@
 trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
 trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab)
 
+trans-⊂ :  { A B C : HOD} → A ⊂ B → B ⊂ C → A ⊂ C
+trans-⊂ ⟪ A<B , A⊆B ⟫ ⟪ B<C , B⊆C ⟫ = ⟪ ordtrans A<B B<C , (λ ab → B⊆C (A⊆B ab)) ⟫
+
 refl-⊆ : {A : HOD} → A ⊆ A
 refl-⊆ x = x
 
--- a/src/filter.agda	Tue Jan 10 02:19:08 2023 +0900
+++ b/src/filter.agda	Tue Jan 10 03:00:04 2023 +0900
@@ -216,7 +216,7 @@
              Ly = subst (λ k → odef L k) (sym &iso) (f⊆L mf mfy)
              mu08 : L ∋ y+q-r
              mu08 = CUP Ly (NEG Lq (subst (λ k → odef L k) 
-               (trans (cong (λ k → & (* y ∪ k)) (sym *iso)) (sym x=y∪p) ) (CUP Ly Lp )) ) where
+               (trans (cong (λ k → & (* y ∪ k)) (sym *iso)) (sym x=y∪p) ) (CUP Ly Lp )) ) 
              mu09 : * y ⊆ y+q-r
              mu09 {x} yx = case1 yx
              mu07 : filter mf  ∋ y+q-r
@@ -296,21 +296,31 @@
      f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) )
 
 import zorn 
-open zorn O _⊆_ 
+
+open import Relation.Binary
+
+PO : IsStrictPartialOrder _≡_ _⊂_ 
+PO = record { isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
+   ; trans = λ {a} {b} {c} → trans-⊂ {a} {b} {c}
+   ; irrefl = λ x=y x<y → ?
+   ; <-resp-≈ =  record { fst = λ {x} {y} {y1} y=y1 xy1 → ? ; snd = λ {x} {x1} {y} x=x1 x1y → ? } }
+
+open zorn O _⊂_ PO
 
 open import  Relation.Binary.Structures
 
+SUP⊆ : (P B : HOD) → B ⊆ P → IsTotalOrderSet B → SUP P B
+SUP⊆ P B B⊆P OB = record { sup = Union B ; isSUP = record { ax = ? ; x≤sup = ? } }
+
 MaximumSubset : {L P : HOD} 
       → o∅ o< & L →  o∅ o< & P → P ⊆ L
-      → (PO : IsStrictPartialOrder _≡_ _⊆_ )
-      → ( (B : HOD) → B ⊆ P → IsTotalOrderSet PO B  → SUP PO P B  )
-      → Maximal PO P
-MaximumSubset {L} {P} 0<L 0<P P⊆L PO C = Zorn-lemma PO 0<P {!!}
+      → Maximal  P
+MaximumSubset {L} {P} 0<L 0<P P⊆L = Zorn-lemma 0<P (SUP⊆ P)
 
 MaximumFilterExist : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p)) → ({p q : HOD} → L ∋ p → L ∋ q → L ∋ (p ∩ q))
       → (F : Filter {L} {P} LP) → o∅ o< & L →  o∅ o< & (filter F)  →  (¬ (filter F ∋ od∅)) → MaximumFilter {L} {P} LP 
 MaximumFilterExist {L} {P} LP NEG CAP F 0<L 0<F Fprop = record { mf = {!!} ; proper = {!!} ; is-maximum = {!!} }  where
-     mf01 : Maximal  {!!}  {!!}
-     mf01 = MaximumSubset  0<L {!!}  {!!} {!!}  {!!}
+     mf01 : Maximal  {!!}  
+     mf01 = MaximumSubset  0<L {!!} {!!}