Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 934:ebcad8e5ae55
resync zorn.agda
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 24 Oct 2022 09:36:07 +0900 |
| parents | 409ac0af7b3b |
| children | ed711d7be191 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 49 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 24 09:15:49 2022 +0900 +++ b/src/zorn.agda Mon Oct 24 09:36:07 2022 +0900 @@ -413,9 +413,12 @@ chain = UnionCF A f mf ay supf z chain⊆A : chain ⊆' A chain⊆A = λ lt → proj1 lt + sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) sup {x} x≤z = M→S supf (minsup x≤z) - -- supf-sup<minsup : {x : Ordinal } → (x≤z : x o≤ z) → & (SUP.sup (M→S supf (minsup x≤z) )) o≤ supf x ... supf-mono + + s=ms : {x : Ordinal } → (x≤z : x o≤ z ) → & (SUP.sup (sup x≤z)) ≡ MinSUP.sup (minsup x≤z) + s=ms {x} x≤z = &iso chain∋init : odef chain y chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ @@ -1331,19 +1334,19 @@ → Tri (* ua < * ub) (* ua ≡ * ub) (* ub < * ua ) uz01 {ua} {ub} (zchain uza uca) (zchain uzb ucb) = chain-total A f mf ay supf (proj2 uca) (proj2 ucb) - usp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) - → ( supf : Ordinal → Ordinal ) - → SUP A (UnionZF f mf ay supf ) - usp0 f mf ay supf = supP (UnionZF f mf ay supf ) (λ lt → auzc f mf ay supf lt ) (uzctotal f mf ay supf ) + msp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) + → (zc : ZChain A f mf ay x ) + → MinSUP A (UnionCF A f mf ay (ZChain.supf zc) x) + msp0 f mf {x} ay zc = minsupP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where + ztotal : IsTotalOrderSet (ZChain.chain zc) + ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) + uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) → (zc : ZChain A f mf ay x ) → SUP A (UnionCF A f mf ay (ZChain.supf zc) x) - sp0 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where - ztotal : IsTotalOrderSet (ZChain.chain zc) - ztotal {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where - uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) - uz01 = chain-total A f mf ay (ZChain.supf zc) ( (proj2 ca)) ( (proj2 cb)) + sp0 f mf ay zc = M→S (ZChain.supf zc) (msp0 f mf ay zc ) fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) → ZChain.supf zc (& (SUP.sup (sp0 f mf as0 zc))) o< ZChain.supf zc (& A) @@ -1411,12 +1414,18 @@ (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc ss<sa ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x supf = ZChain.supf zc + msp1 : MinSUP A (ZChain.chain zc) + msp1 = msp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc sp1 : SUP A (ZChain.chain zc) sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc - c = & (SUP.sup sp1) - z20 : c << cf nmx c - z20 = proj1 (cf-is-<-monotonic nmx c (SUP.as sp1) ) - asc : odef A (supf c) + c : Ordinal + c = & ( SUP.sup sp1 ) + mc = MinSUP.sup msp1 + c=mc : c ≡ mc + c=mc = &iso + z20 : mc << cf nmx mc + z20 = proj1 (cf-is-<-monotonic nmx mc (MinSUP.asm msp1) ) + asc : odef A (supf mc) asc = ZChain.asupf zc spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) spd = ysup (cf nmx) (cf-is-≤-monotonic nmx) asc @@ -1453,20 +1462,36 @@ -- z25 : {x : Ordinal } → odef (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc ) x → (x ≡ y ) ∨ (x << y ) -- z25 {x} (init au eq ) = ? -- sup c = x, cf y ≡ d, sup c =< d -- z25 (fsuc x lt) = ? -- cf (sup c) + sd=d : supf d ≡ d sd=d = ZChain.sup=u zc (MinSUP.asm spd) (o<→≤ d<A) ⟪ is-sup , not-hasprev ⟫ - sc<sd : supf c << supf d - sc<sd = ? - -- z21 = proj1 ( cf-is-<-monotonic nmx ? ? ) - -- sco<d : supf c o< supf d - -- sco<d with osuc-≡< ( ZChain.supf-<= zc (case2 sc<sd ) ) - -- ... | case1 eq = ⊥-elim ( <-irr eq sc<sd ) - -- ... | case2 lt = lt + + sc<<d : {mc : Ordinal } → {asc : odef A (supf mc)} → (spd : MinSUP A (uchain (cf nmx) (cf-is-≤-monotonic nmx) asc )) + → supf mc << MinSUP.sup spd + sc<<d {mc} {asc} spd = z25 where + d1 : Ordinal + d1 = MinSUP.sup spd + z24 : (supf mc ≡ d1) ∨ ( supf mc << d1 ) + z24 = MinSUP.x<sup spd (init asc refl) + z25 : supf mc << d1 + z25 with z24 + ... | case2 lt = lt + ... | case1 eq = ? + + sc<sd : {mc d : Ordinal } → supf mc << supf d → supf mc o< supf d + sc<sd {mc} {d} sc<<sd with osuc-≡< ( ZChain.supf-<= zc (case2 sc<<sd ) ) + ... | case1 eq = ⊥-elim ( <-irr (case1 (cong (*) (sym eq) )) sc<<sd ) + ... | case2 lt = lt + + sms<sa : supf mc o< supf (& A) + sms<sa with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ MinSUP.asm msp1 , lift true ⟫) )) + ... | case2 lt = lt + ... | case1 eq = ⊥-elim ( o<¬≡ eq ( ordtrans<-≤ (sc<sd (subst (λ k → supf mc << k ) (sym sd=d) (sc<<d {mc} {asc} spd)) ) + ( ZChain.supf-mono zc (o<→≤ d<A )))) ss<sa : supf c o< supf (& A) - ss<sa = ? -- with osuc-≡< ( ZChain.supf-mono zc (o<→≤ ( ∈∧P→o< ⟪ SUP.as sp0 , lift true ⟫) )) - -- ... | case2 lt = lt - -- ... | case1 eq = ? -- where + ss<sa = subst (λ k → supf k o< supf (& A)) (sym c=mc) sms<sa + 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