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

changeset 928:330303f0c688

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 Sat, 22 Oct 2022 11:15:17 +0900
parents 0f2a85826cc7
children a6d97e6e5309
files src/zorn.agda
diffstat 1 files changed, 25 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/src/zorn.agda	Fri Oct 21 07:57:07 2022 +0900
+++ b/src/zorn.agda	Sat Oct 22 11:15:17 2022 +0900
@@ -696,8 +696,8 @@
                uz01 = fcn-cmp y f mf ca cb
 
      ysup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) 
-       →  SUP A (uchain f mf ay)
-     ysup f mf {y} ay = supP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
+       →  MinSUP A (uchain f mf ay)
+     ysup f mf {y} ay = minsupP (uchain f mf ay) (λ lt → A∋fc y f mf lt)  (utotal f mf ay) 
 
      SUP⊆ : { B C : HOD } → B ⊆' C → SUP A C → SUP A B
      SUP⊆ {B} {C} B⊆C sup = record { sup = SUP.sup sup ; as = SUP.as sup ; x<sup = λ lt → SUP.x<sup sup (B⊆C lt)    }
@@ -1197,7 +1197,7 @@
           pzc : (z : Ordinal) → z o< x → ZChain A f mf ay z
           pzc z z<x = prev z z<x
 
-          ysp =  & (SUP.sup (ysup f mf ay))
+          ysp =  MinSUP.sup (ysup f mf ay)
 
           supf0 : Ordinal → Ordinal
           supf0 z with trio< z x
@@ -1414,14 +1414,29 @@
           sp1 : SUP A (ZChain.chain zc)
           sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 
           c = & (SUP.sup sp1)
-          d : Ordinal
-          d = cf nmx (supf c )
-          z21 : d o< & A
-          z21 =  ∈∧P→o< ⟪ proj2 (cf-is-<-monotonic nmx (supf c) (ZChain.asupf zc))  , lift true ⟫
-          z20 : supf c << d
-          z20 = proj1 (cf-is-<-monotonic nmx (supf c) (ZChain.asupf zc) )
+          z20 : c << cf nmx c 
+          z20 = proj1 (cf-is-<-monotonic nmx c (SUP.as sp1) )
+          asc : odef A (supf c)
+          asc = ZChain.asupf zc
+          spd : MinSUP A (uchain (cf nmx)  (cf-is-≤-monotonic nmx) asc ) 
+          spd = ysup (cf nmx)  (cf-is-≤-monotonic nmx) asc
+          d = MinSUP.sup spd
+          d<A : d o< & A
+          d<A =  ∈∧P→o< ⟪ MinSUP.asm spd , lift true ⟫
+          sd=ms : supf d ≡ MinSUP.sup ( ZChain.minsup zc (o<→≤ d<A) )
+          sd=ms = ZChain.supf-is-minsup zc (o<→≤ d<A)
+          sd=d : supf d ≡ d
+          sd=d = ?
+          sc<d : supf c << d
+          sc<d = ? where
+              z21 = proj1 ( cf-is-<-monotonic nmx ? ? )
+          sco<d : supf c o< supf d
+          sco<d = ?
+
           ss<sa : supf c o< supf (& A)
-          ss<sa = ?
+          ss<sa with osuc-≡< ( ZChain.supf-mono zc ? )
+          ... | case2 lt = lt
+          ... | case1 eq = ? -- where
      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)) ; as = zorn01 ; ¬maximal<x  = zorn02 } where