Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 924:a48dc906796c
supf usp0 instead of supf (& A) ?
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 19 Oct 2022 09:10:27 +0900 |
| parents | 85f6238a38db |
| children | babd8ac79a91 |
| files | src/zorn.agda |
| diffstat | 1 files changed, 46 insertions(+), 46 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Oct 19 08:41:42 2022 +0900 +++ b/src/zorn.agda Wed Oct 19 09:10:27 2022 +0900 @@ -1316,33 +1316,31 @@ 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) + usp0 : ( 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 supf = supP (UnionZF f mf ay supf ) (λ lt → ? ) (uztotal f mf ay supf ) + usp0 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) + 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) - sp00 f mf {x} ay zc = supP (UnionCF A f mf ay (ZChain.supf zc) x) (ZChain.chain⊆A zc) ztotal where + 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)) - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) - → f (& (SUP.sup (sp0 f mf as0 ? ))) ≡ & (SUP.sup (sp0 f mf as0 ? )) - fixpoint f mf = z14 where - chain = UnionZF f mf as0 ? - supf : Ordinal → Ordinal - supf = ? - sp1 : SUP A ? - sp1 = sp0 f mf as0 ? + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A f mf as0 (& A) ) + → f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) + fixpoint f mf zc = z14 where + chain = ZChain.chain zc + supf = ZChain.supf zc + sp1 : SUP A chain + sp1 = sp0 f mf as0 zc 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 - z10 = ? -- ZChain1.is-max (SZ1 f mf as0 zc (& A) ) + z10 = ZChain1.is-max (SZ1 f mf as0 zc (& A) ) z22 : & (SUP.sup sp1) o< & A z22 = c<→o< ( SUP.as sp1 ) z21 : supf (& (SUP.sup sp1)) o< supf (& A) @@ -1351,52 +1349,54 @@ -- z21 = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k) (sym &iso) (ZChain.asupf zc ) )) z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) - ... | yes eq = subst (λ k → odef chain k) eq ? -- ( ZChain.chain∋init zc ) - ... | no ne = ? where -- ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) - -- (case2 ? ) z13 where + ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) + ... | no ne = ZChain1.is-max (SZ1 f mf as0 zc (& A)) {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) z21 (SUP.as sp1) + (case2 z19 ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) - z13 with SUP.x<sup sp1 ? + z13 with SUP.x<sup sp1 ( ZChain.chain∋init zc ) ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt z19 : IsSup A chain {& (SUP.sup sp1)} (SUP.as sp1) z19 = record { x<sup = z20 } where z20 : {y : Ordinal} → odef chain y → (y ≡ & (SUP.sup sp1)) ∨ (y << & (SUP.sup sp1)) - z20 {y} zy with SUP.x<sup sp1 ? + z20 {y} zy with SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) zy) ... | 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 = ? -- with ? --- ... | tri< a ¬b ¬c = ⊥-elim z16 where --- z16 : ⊥ --- z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) --- ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) --- ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) --- ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) --- ... | tri> ¬a ¬b c = ⊥-elim z17 where --- z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) --- z15 = SUP.x<sup sp1 ? -- (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) --- z17 : ⊥ --- z17 with z15 --- ... | case1 eq = ¬b eq --- ... | case2 lt = ¬a lt + 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 as0 supf ( (proj2 ca)) ( (proj2 cb)) + z14 : f (& (SUP.sup (sp0 f mf as0 zc ))) ≡ & (SUP.sup (sp0 f mf as0 zc )) + z14 with ztotal (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 + ... | tri< a ¬b ¬c = ⊥-elim z16 where + z16 : ⊥ + z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.as sp1 )) + ... | case1 eq = ⊥-elim (¬b (subst₂ (λ j k → j ≡ k ) refl *iso (sym eq) )) + ... | case2 lt = ⊥-elim (¬c (subst₂ (λ j k → k < j ) refl *iso lt )) + ... | tri≈ ¬a b ¬c = subst ( λ k → k ≡ & (SUP.sup sp1) ) &iso ( cong (&) b ) + ... | tri> ¬a ¬b c = ⊥-elim z17 where + z15 : (* (f ( & ( SUP.sup sp1 ))) ≡ SUP.sup sp1) ∨ (* (f ( & ( SUP.sup sp1 ))) < SUP.sup sp1) + z15 = SUP.x<sup sp1 (subst (λ k → odef chain k ) (sym &iso) (ZChain.f-next zc z12 )) + z17 : ⊥ + z17 with z15 + ... | case1 eq = ¬b eq + ... | case2 lt = ¬a lt + -- ZChain contradicts ¬ Maximal -- -- ZChain forces fix point on any ≤-monotonic function (fixpoint) -- ¬ Maximal create cf which is a <-monotonic function by axiom of choice. This contradicts fix point of ZChain -- - z04 : (nmx : ¬ Maximal A ) → ⊥ - 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 ) ) + + z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) → ⊥ + z04 nmx zc = <-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 ) zc ))) -- x ≡ f x ̄ + (proj1 (cf-is-<-monotonic nmx c (SUP.as sp1 ))) where -- x < f x + sp1 : SUP A (ZChain.chain zc) + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) as0 zc 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 @@ -1407,7 +1407,7 @@ zorn01 = proj1 zorn03 zorn02 : {x : HOD} → A ∋ x → ¬ (ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) (sym *iso) (sym *iso) m<x ) - ... | yes ¬Maximal = ⊥-elim ( z04 nmx ) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx ? ) where -- if we have no maximal, make ZChain, which contradict SUP condition nmx : ¬ Maximal A nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where