Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 923:85f6238a38db
use supf of zchain for (nmx : ¬ Maximal A ) → ⊥
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 19 Oct 2022 08:41:42 +0900 |
| parents | 620c2f3440f5 |
| children | a48dc906796c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 32 insertions(+), 24 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Oct 17 11:29:37 2022 +0900 +++ b/src/zorn.agda Wed Oct 19 08:41:42 2022 +0900 @@ -1300,40 +1300,45 @@ SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain A f mf ay x SZ f mf {y} ay x = TransFinite {λ z → ZChain A f mf ay z } (λ x → ind f mf ay x ) x - record ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) (z : Ordinal) : Set n where - field - uz : Ordinal - zc : odef (ZChain.chain (SZ f mf ay uz)) z + data ZChainP ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) + ( supf : Ordinal → Ordinal ) (z : Ordinal) : Set n where + zchain : (uz : Ordinal ) → odef (UnionCF A f mf ay supf uz) z → ZChainP f mf ay supf z - UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → HOD - UnionZF f mf {y} ay = record { od = record { def = λ x → ZChainP f mf ay x } ; odmax = & A ; <odmax = λ lt → ∈∧P→o< ( ZChainP.zc lt) } + UnionZF : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) + (supf : Ordinal → Ordinal ) → HOD + UnionZF f mf {y} ay supf = record { od = record { def = λ x → ZChainP f mf ay supf x } + ; odmax = & A ; <odmax = λ lt → ∈∧P→o< ? } - uztotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → - IsTotalOrderSet (UnionZF f mf ay) - uztotal f mf ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + uztotal : ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) + → ( supf : Ordinal → Ordinal ) + → IsTotalOrderSet (UnionZF f mf ay supf ) + uztotal f mf ay sz {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 = ? - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) → SUP A (UnionZF f mf ay ) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {x y : Ordinal} (ay : odef A y) + → ( supf : Ordinal → Ordinal ) + → SUP A (UnionZF f mf ay supf ) -- sp0 f mf {x} ay = supP (UnionZF f mf ay ) (λ lt → proj1 (ZChainP.zc lt)) (uztotal f mf ay) - sp0 f mf {x} ay = ? -- supP ? ? ? + sp0 f mf {x} ay supf = supP (UnionZF f mf ay supf ) (λ lt → ? ) (uztotal f mf ay supf ) sp00 : ( 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) - sp00 f mf ay zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ztotal where + → (zc : ZChain A f mf ay x ) + → SUP A (UnionCF A f mf ay (ZChain.supf zc) x) + sp00 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)) fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) - → f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 )) + → f (& (SUP.sup (sp0 f mf as0 ? ))) ≡ & (SUP.sup (sp0 f mf as0 ? )) fixpoint f mf = z14 where - chain = UnionZF f mf as0 + chain = UnionZF f mf as0 ? supf : Ordinal → Ordinal supf = ? sp1 : SUP A ? - sp1 = sp0 f mf as0 + sp1 = sp0 f mf as0 ? z10 : {a b : Ordinal } → (ca : odef chain a ) → supf b o< supf (& A) → (ab : odef A b ) → HasPrev A chain b f ∨ IsSup A chain {b} ab → * a < * b → odef chain b @@ -1359,7 +1364,7 @@ z20 {y} zy with SUP.x<sup sp1 ? ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) - z14 : f (& (SUP.sup (sp0 f mf as0 ))) ≡ & (SUP.sup (sp0 f mf as0 )) + z14 : f (& (SUP.sup (sp0 f mf as0 ? ))) ≡ & (SUP.sup (sp0 f mf as0 ? )) z14 = ? -- with ? -- ... | tri< a ¬b ¬c = ⊥-elim z16 where -- z16 : ⊥ @@ -1381,14 +1386,17 @@ -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain -- z04 : (nmx : ¬ Maximal A ) → ⊥ - z04 nmx = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.as sp1 )))) - (subst (λ k → odef A (& k)) (sym *iso) (SUP.as sp1) ) - (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) ))) -- x ≡ f x ̄ - (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x - sp1 : SUP A ? - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 + z04 nmx = ? where -- <-irr0 ? ? + --(case1 ?) -- x ≡ f x ̄ + -- ? where -- x < f x + sp1 : SUP A ? + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 ? + z041 : ? + z041 = cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) ) c = & (SUP.sup sp1) - + z042 : ? + z042 = is-cf nmx (SUP.as ? ) + z043 = proj1 (cf-is-<-monotonic nmx ? (SUP.as ? )) 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