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

changeset 553:567a1a9f3e0a

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, 28 Apr 2022 19:00:40 +0900
parents fb210e812eba
children 0687736285ce
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 11 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Thu Apr 28 18:33:10 2022 +0900
+++ b/src/zorn.agda	Thu Apr 28 19:00:40 2022 +0900
@@ -216,11 +216,6 @@
      --       ∨  (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ x)
      --       ∨ ( ( z : Ordinal) → odef (ZChain.chain zc0) z → ¬ ( * z < * x ))
      -- 3cases {x} {y} f mf ax ay zc0 = {!!}
-     -- Union of ZFChain
-     UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) 
-            → ( (z : Ordinal) → z o< B → {y : Ordinal} →  (ya : odef A y) → ZChain A ya f mf supO z ) → HOD
-     UZFChain f mf B prev = record { od = record { def = λ y → odef A y ∧ (y o< B)  ∧ ( (y<b : y o< B) → (ya : odef A y) → odef (ZChain.chain (prev y y<b ya )) y) }
-         ; odmax = & A ; <odmax = z07 }
      -- create all ZChains under o< x
      ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) →
             ((z : Ordinal) → z o< x → {y : Ordinal} → (ya : odef A y) → ZChain A ya f mf supO z ) → { y : Ordinal } → (ya : odef A y) → ZChain A ya f mf supO x
@@ -272,13 +267,18 @@
                             * a < * b → odef (ZChain.chain zc0) b
                 z18 {a} {b} za b<x ba (case1 p) a<b = {!!}
                 z18 {a} {b} za b<x ba (case2 p) a<b = {!!}
-     ... | no ¬ox with trio< (& A) x   --- limit ordinal case
-     ... | tri< a ¬b ¬c = {!!} where
-          zc0 = prev (& A) a
-     ... | tri≈ ¬a b ¬c = {!!}
-     ... | tri> ¬a ¬b c =  {!!} where
+     ... | no ¬ox =  {!!}  where --- limit ordinal case
+     -- Union of ZFChain
+         record UZFChain (y : Ordinal) : Set n where
+            field
+               u : Ordinal
+               u<x : u o< x
+               zuy : odef (ZChain.chain (prev u u<x ay )) y
          uzc : HOD
-         uzc = UZFChain f mf x prev
+         uzc = record { od = record { def = λ y → UZFChain y } ; odmax = & A ; <odmax = {!!} }
+         u-total : IsTotalOrderSet uzc
+         u-total {x} {y} ux uy = {!!}
+         
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM 
      ... | no not = record { maximal = ODC.minimal O HasMaximal  (λ eq → not (=od∅→≡o∅ eq)) ; A∋maximal = zorn01 ; ¬maximal<x  = zorn02 } where