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

changeset 636:844eb13a5a39

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, 21 Jun 2022 11:03:20 +0900
parents 761bf71e5594
children c17d46ecb051
files src/zorn.agda
diffstat 1 files changed, 11 insertions(+), 18 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Tue Jun 21 10:07:58 2022 +0900
+++ b/src/zorn.agda	Tue Jun 21 11:03:20 2022 +0900
@@ -667,10 +667,12 @@
          ... | case1 z=y  = subst (λ k → x o< k ) z=y x<z
          ... | case2 z<y  = ordtrans x<z z<y
          u-mono : {z : Ordinal} → z o≤ x → supf0 z ⊆' supf0 x
-         u-mono {z} z≤x {i} with trio< z x 
-         ... | tri< a ¬b ¬c = {!!} -- λ lt → lt -- record { u = z ; u<x = a ; chain∋z = lt }
-         ... | tri≈ ¬a b ¬c = {!!} -- λ lt → lt 
-         ... | tri> ¬a ¬b c = {!!} -- λ lt → lt 
+         u-mono {z} z≤x {i} with trio< z x | trio< x x
+         ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = λ lt → {!!}
+         ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = {!!} ; u<x = {!!} ;  chain∋z = lt }
+         ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = λ lt → {!!}
+         ... | tri≈ ¬a b ¬c | s = {!!} -- λ lt → lt 
+         ... | tri> ¬a ¬b c | s = {!!} -- λ lt → lt 
          
      SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A)
      SZ f mf {y} ay = TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) (& A)
@@ -691,20 +693,11 @@
      SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y)
          → (z : Ordinal) → ZChain1 f mf ay z
      SZ1 f mf {y} ay z = record { zc = TransFinite {λ z → ZChain A y f z  } (ind f mf ay ) z
-             ; chain-mono = {!!} ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where
-         indp :  (x : Ordinal) →
-            ((y₁ : Ordinal) → y₁ o< x → ZChain1 f mf ay y₁) →
-            ZChain1 f mf ay x
-         indp x prev with Oprev-p x
-         ... | yes op  = sz02 where
-             sz02 : ZChain1 f mf ay x
-             sz02 with ODC.∋-p O A (* x)
-             ... | no noax = {!!}
-             ... | yes noax = {!!}
-         ... | no  ¬ox  with trio< x y
-         ... | tri< a ¬b ¬c = {!!}
-         ... | tri≈ ¬a b ¬c = {!!}
-         ... | tri> ¬a ¬b y<x = {!!}
+             ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where
+         sf : Ordinal → HOD
+         sf x = ZChain.supf (TransFinite (ind f mf ay) z) x
+         mono :  {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → w o≤ z → sf x ⊆' sf w 
+         mono {a} {b} sf a≤b b≤z = TransFinite0 {λ b → a o≤ b → b o≤ z →  sf a ⊆' sf b } {!!} b a≤b b≤z
 
      zorn00 : Maximal A 
      zorn00 with is-o∅ ( & HasMaximal )  -- we have no Level (suc n) LEM