Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 546:3234a5f6bfcf
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 27 Apr 2022 11:01:43 +0900 |
| parents | f8eb56442f2c |
| children | 379bd9b4610c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 54 insertions(+), 87 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Wed Apr 27 09:08:25 2022 +0900 +++ b/src/zorn.agda Wed Apr 27 11:01:43 2022 +0900 @@ -191,17 +191,16 @@ SupCond : ( A B : HOD) → (B⊆A : B ⊆ A) → IsTotalOrderSet B → Set (Level.suc n) SupCond A B _ _ = SUP A B -record ZChain ( A : HOD ) {x : Ordinal} (ax : A ∋ * x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) - (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) (z : Ordinal) : Set (Level.suc n) where +record ZChain ( A : HOD ) {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) + (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) : Set (Level.suc n) where field chain : HOD chain⊆A : chain ⊆ A chain∋x : odef chain x - ¬chain∋x>z : { a : Ordinal } → z o< osuc a → ¬ odef chain a f-total : IsTotalOrderSet chain - f-next : {a : Ordinal } → odef chain a → a o< z → odef chain (f a) + f-next : {a : Ordinal } → odef chain a → odef chain (f a) f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) - is-max : {a b : Ordinal } → (ca : odef chain a ) → (ba : odef A b) → a o< z + is-max : {a b : Ordinal } → (ca : odef chain a ) → (ba : odef A b) → Prev< A chain ba f ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ) → * a < * b → odef chain b @@ -224,8 +223,6 @@ s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) sa : A ∋ * ( & s ) sa = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) - sa0 : odef A (& s) - sa0 = subst (λ k → odef A (& k) ) {!!} ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) HasMaximal : HOD HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) → odef A m → ¬ (* x < * m)) } ; odmax = & A ; <odmax = z07 } no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → odef A x ∧ ((m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m) )) → ⊥ @@ -259,12 +256,12 @@ cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫ - zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf supO (& A)) → SUP A (ZChain.chain zc) + zsup : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f) → (zc : ZChain A sa f mf supO ) → SUP A (ZChain.chain zc) zsup f mf zc = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc ) - A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) + A∋zsup : (nmx : ¬ Maximal A ) (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO ) → A ∋ * ( & ( SUP.sup (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) )) A∋zsup nmx zc = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup (cf nmx) (cf-is-≤-monotonic nmx) zc ) ) - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) → SUP A (* (& (ZChain.chain zc))) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO ) → SUP A (* (& (ZChain.chain zc))) sp0 f mf zc = supP (* (& (ZChain.chain zc))) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc)) (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc) ) zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P @@ -273,12 +270,12 @@ --- --- sup is fix point in maximum chain --- - z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A sa f mf supO (& A)) - → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc )) + z03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) f mf supO ) + → f (& (SUP.sup (sp0 f mf zc ))) ≡ & (SUP.sup (sp0 f mf zc )) z03 f mf zc = z14 where chain = ZChain.chain zc sp1 = sp0 f mf zc - z10 : {a b : Ordinal } → (ca : odef chain a ) → (ab : odef A b ) → a o< (& A) + z10 : {a b : Ordinal } → (ca : odef chain a ) → (ab : odef A b ) → Prev< A chain ab f ∨ (supO (& chain) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc)) (subst (λ k → IsTotalOrderSet k) (sym *iso) (ZChain.f-total zc)) ≡ b ) → * a < * b → odef chain b @@ -288,13 +285,13 @@ z12 : odef chain (& (SUP.sup sp1)) z12 with o≡? (& s) (& (SUP.sup sp1)) ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋x zc ) - ... | no ne = z10 {& s} {& (SUP.sup sp1)} (ZChain.chain∋x zc) (SUP.A∋maximal sp1) (c<→o< (subst (λ k → odef A (& k) ) *iso sa) ) (case2 refl ) z13 where + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋x zc ) (SUP.A∋maximal sp1) (case2 refl ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) z13 with SUP.x<sup sp1 (subst (λ k → odef k (& s)) (sym *iso) ( ZChain.chain∋x zc )) ... | case1 eq = ⊥-elim ( ne (cong (&) eq) ) ... | case2 lt = subst₂ (λ j k → j < k ) (sym *iso) (sym *iso) lt z14 : f (& (SUP.sup (sp0 f mf zc))) ≡ & (SUP.sup (sp0 f mf zc)) - z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 z11 ))) (me z12 ) + z14 with IsStrictTotalOrder.compare (ZChain.f-total zc ) (me (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 ))) (me z12 ) ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ z16 with proj1 (mf (& ( SUP.sup sp1)) ( SUP.A∋maximal sp1 )) @@ -303,83 +300,71 @@ ... | 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₂ (λ j k → odef j k ) (sym *iso) (sym &iso) (ZChain.f-next zc z12 z11 ) ) + z15 = SUP.x<sup sp1 (subst₂ (λ j k → odef j k ) (sym *iso) (sym &iso) (ZChain.f-next zc z12 )) z17 : ⊥ z17 with z15 ... | case1 eq = ¬b eq ... | case2 lt = ¬a lt - z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A sa (cf nmx) (cf-is-≤-monotonic nmx) supO (& A)) → ⊥ + z04 : (nmx : ¬ Maximal A ) → (zc : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO ) → ⊥ z04 nmx zc = z01 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1)))) (subst (λ k → odef A (& k)) (sym *iso) (SUP.A∋maximal sp1) ) (case1 ( cong (*)( z03 (cf nmx) (cf-is-≤-monotonic nmx ) zc ))) (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1))) where - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc c = & (SUP.sup sp1) - premax : {x y : Ordinal} → y o< x → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain A sa f mf supO y ) + premax : {x y : Ordinal} → y o< x → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain A sa f mf supO ) → {a b : Ordinal} (ca : odef (ZChain.chain zc0) a) → (ab : odef A b) → a o< y → Prev< A (ZChain.chain zc0) ab f ∨ (supO (& (ZChain.chain zc0)) (subst (λ k → k ⊆ A) (sym *iso) (ZChain.chain⊆A zc0)) (subst IsTotalOrderSet (sym *iso) (ZChain.f-total zc0)) ≡ b) → * a < * b → odef (ZChain.chain zc0) b - premax {x} {y} y<x f mf zc0 {a} {b} ca ab a<y P a<b = ZChain.is-max zc0 ca ab a<y P a<b + premax {x} {y} y<x f mf zc0 {a} {b} ca ab a<y P a<b = ZChain.is-max zc0 ca ab P a<b -- ca ab y P a<b -- Union of ZFChain UZFChain : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (B : Ordinal) - → ( (y : Ordinal) → y o< B → ZChain A sa f mf supO y ) → HOD - UZFChain f mf B prev = record { od = record { def = λ y → odef A y ∧ (y o< B) ∧ ( (y<b : y o< B) → odef (ZChain.chain (prev y y<b)) y) } + → ( (y : Ordinal) → y o< B → (ya : odef A y) → ZChain A ya f mf supO ) → HOD + UZFChain f mf B prev = record { od = record { def = λ y → odef A y ∧ (y o< B) ∧ ( (y<b : y o< B) → (ya : odef A y) → odef (ZChain.chain (prev y y<b ya )) y) } ; odmax = & A ; <odmax = z07 } -- ZChain is not compatible with the SUP condition - ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa f mf supO y ) - → ZChain A sa f mf supO x - ind f mf x prev with Oprev-p x - ... | yes op with ODC.∋-p O A (* x) - ... | no ¬Ax = zc1 where - -- we have previous ordinal and ¬ A ∋ x, use previous Zchain + ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → + ((y : Ordinal) → y o< x → (ya : odef A y) → ZChain A ya f mf supO) → (ya : odef A x) → ZChain A ya f mf supO + ind f mf x prev ax with Oprev-p x + ... | yes op with ODC.∋-p O A (* (Oprev.oprev op)) + ... | yes apx = zc4 where -- we have previous ordinal and A ∋ op px = Oprev.oprev op - zc0 : ZChain A sa f mf supO (Oprev.oprev op) - zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) - zc1 : ZChain A sa f mf supO x - zc1 = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 - ; f-next = zc20 (ZChain.f-next zc0) ; f-immediate = ZChain.f-immediate zc0 - ; ¬chain∋x>z = λ {a} x<oa → ZChain.¬chain∋x>z zc0 (ordtrans (subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc ) x<oa ) - ; chain∋x = ZChain.chain∋x zc0 ; is-max = λ za ba a<x → zc20 (λ za a<x → ZChain.is-max zc0 za ba a<x ) za a<x } where - zc20 : {P : Ordinal → Set n} → ({a : Ordinal} → odef (ZChain.chain zc0) a → a o< px → P a) - → {a : Ordinal} → (za : odef (ZChain.chain zc0) a ) → (a<x : a o< x) → P a - zc20 {P} prev {a} za a<x with trio< a px - ... | tri< a₁ ¬b ¬c = prev za a₁ - ... | tri≈ ¬a b ¬c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (subst (λ k → k o< osuc a) b <-osuc ) za ) - ... | tri> ¬a ¬b c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (ordtrans c <-osuc ) za ) - ... | yes ax = zc4 where -- we have previous ordinal and A ∋ x - px = Oprev.oprev op - zc0 : ZChain A sa f mf supO (Oprev.oprev op) - zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc) + apx0 = subst (λ k → odef A k ) &iso apx + zc0 : ZChain A apx0 f mf supO + zc0 = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) apx0 + ax0 : odef A (& (* x)) + ax0 = {!!} Afx : { x : Ordinal } → A ∋ * x → A ∋ * (f x) Afx {x} ax = (subst (λ k → odef A k ) (sym &iso) (proj2 (mf x (subst (λ k → odef A k ) &iso ax)))) -- x is in the previous chain, use the same -- x has some y which y < x ∧ f y ≡ x -- x has no y which y < x - zc4 : ZChain A sa f mf supO x + zc4 : ZChain A ax f mf supO zc4 with ODC.p∨¬p O ( Prev< A (ZChain.chain zc0) ax f ) ... | case1 y = zc7 where -- we have previous < chain = ZChain.chain zc0 - zc7 : ZChain A sa f mf supO x + zc7 : ZChain A ax f mf supO zc7 with ODC.∋-p O (ZChain.chain zc0) (* ( f x ) ) - ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = zc20 (ZChain.f-next zc0) - ; f-immediate = ZChain.f-immediate zc0 ; ¬chain∋x>z = z22 ; chain∋x = ZChain.chain∋x zc0 ; is-max = λ za ba a<x → zc20 (λ za a<x → ZChain.is-max zc0 za ba a<x ) za a<x } where -- no extention + ... | yes y = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = ZChain.f-next zc0 + ; f-immediate = ZChain.f-immediate zc0 ; chain∋x = {!!} -- ZChain.chain∋x zc0 + ; is-max = {!!} } where -- no extention z22 : {a : Ordinal} → x o< osuc a → ¬ odef (ZChain.chain zc0) a - z22 {a} x<oa = ZChain.¬chain∋x>z zc0 (ordtrans (subst (λ k → px o< k ) (Oprev.oprev=x op) <-osuc ) x<oa ) + z22 {a} x<oa = {!!} zc20 : {P : Ordinal → Set n} → ({a : Ordinal} → odef (ZChain.chain zc0) a → a o< px → P a) → {a : Ordinal} → (za : odef (ZChain.chain zc0) a ) → (a<x : a o< x) → P a zc20 {P} prev {a} za a<x with trio< a px ... | tri< a₁ ¬b ¬c = prev za a₁ - ... | tri≈ ¬a b ¬c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (subst (λ k → k o< osuc a) b <-osuc ) za ) - ... | tri> ¬a ¬b c = ⊥-elim ( ZChain.¬chain∋x>z zc0 (ordtrans c <-osuc ) za ) + ... | tri≈ ¬a b ¬c = {!!} + ... | tri> ¬a ¬b c = {!!} z21 : {a : Ordinal} → odef (ZChain.chain zc0) a → a o< x → odef (ZChain.chain zc0) (f a) z21 {a} za a<x with trio< a x - ... | tri< a₁ ¬b ¬c = ZChain.f-next zc0 za {!!} + ... | tri< a₁ ¬b ¬c = ZChain.f-next zc0 za ... | tri≈ ¬a b ¬c = {!!} ... | tri> ¬a ¬b c = ⊥-elim ( o<> c a<x ) ... | no not = record { chain = zc5 ; chain⊆A = ⊆-zc5 - ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = case1 (ZChain.chain∋x zc0) ; ¬chain∋x>z = {!!} ; is-max = {!!} } where + ; f-total = zc6 ; f-next = {!!} ; f-immediate = {!!} ; chain∋x = case1 {!!} ; ¬chain∋x>z = {!!} ; is-max = {!!} } where -- extend with f x -- cahin ∋ y ∧ chain ∋ f y ∧ x ≡ f ( f y ) zc5 : HOD zc5 = record { od = record { def = λ z → odef (ZChain.chain zc0) z ∨ (z ≡ f x) } ; odmax = & A ; <odmax = {!!} } @@ -387,16 +372,16 @@ ⊆-zc5 = record { incl = λ {y} lt → zc15 lt } where zc15 : {z : Ordinal } → ( odef (ZChain.chain zc0) z ∨ (z ≡ f x) ) → odef A z zc15 {z} (case1 zz) = subst (λ k → odef A k ) &iso ( incl (ZChain.chain⊆A zc0) (subst (λ k → odef chain k ) (sym &iso) zz ) ) - zc15 (case2 refl) = proj2 ( mf x (subst (λ k → odef A k ) &iso ax ) ) + zc15 (case2 refl) = proj2 ( mf x (subst (λ k → odef A k ) &iso {!!} ) ) IPO = ⊆-IsPartialOrderSet ⊆-zc5 PO zc8 : { A B x : HOD } → (ax : A ∋ x ) → (P : Prev< A B ax f ) → * (f (& (* (Prev<.y P)))) ≡ x zc8 {A} {B} {x} ax P = subst₂ (λ j k → * ( f j ) ≡ k ) (sym &iso) *iso (sym (cong (*) ( Prev<.x=fy P))) fx=zc : odef (ZChain.chain zc0) x → Tri (* (f x) < * x ) (* (f x) ≡ * x) (* x < * (f x) ) - fx=zc c with mf x (subst (λ k → odef A k) &iso ax ) - ... | ⟪ case1 x=fx , afx ⟫ = tri≈ ( z01 ax (Afx ax) (case1 (sym zc13))) zc13 (z01 (Afx ax) ax (case1 zc13)) where + fx=zc c with mf x (subst (λ k → odef A k) &iso ax0 ) + ... | ⟪ case1 x=fx , afx ⟫ = tri≈ ( z01 ax0 (Afx ax0) (case1 (sym zc13))) zc13 (z01 (Afx ax0) ax0 (case1 zc13)) where zc13 : * (f x) ≡ * x zc13 = subst (λ k → k ≡ * x ) (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym &iso))) (sym ( x=fx )) - ... | ⟪ case2 x<fx , afx ⟫ = tri> (z01 ax (Afx ax) (case2 zc14)) (λ lt → z01 (Afx ax) ax (case1 lt) zc14) zc14 where + ... | ⟪ case2 x<fx , afx ⟫ = tri> (z01 ax0 (Afx ax0) (case2 zc14)) (λ lt → z01 (Afx ax0) ax0 (case1 lt) zc14) zc14 where zc14 : * x < * (f x) zc14 = subst (λ k → * x < k ) (subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym &iso ))) x<fx cmp : Trichotomous _ _ @@ -410,7 +395,7 @@ ... | tri< a₁ ¬b ¬c = {!!} ... | tri≈ ¬a b₁ ¬c = subst₂ (λ j k → Tri ( j < k ) (j ≡ k) ( k < j ) ) zc11 zc10 ( fx=zc zc12 ) where zc10 : * x ≡ b - zc10 = subst₂ (λ j k → j ≡ k ) (zc8 ax y ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) + zc10 = subst₂ (λ j k → j ≡ k ) (zc8 ax {!!} ) (zc8 (incl ( ZChain.chain⊆A zc0 ) c) fb) (cong (λ k → * ( f ( & k ))) b₁) zc11 : * (f x) ≡ a zc11 = subst (λ k → * (f x) ≡ k ) *iso (cong (*) (sym fx)) zc12 : odef chain x @@ -422,15 +407,13 @@ ... | case2 not with ODC.p∨¬p O ( x ≡ & ( SUP.sup ( supP ( ZChain.chain zc0 ) {!!} {!!} ) )) ... | case1 y = {!!} -- x is sup ... | case2 not = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 ; f-next = {!!} - ; f-immediate = {!!} ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } -- no extention - ind f mf x prev | no ¬ox with trio< (& A) x --- limit ordinal case - ... | tri< a ¬b ¬c = record { chain = ZChain.chain zc0 ; chain⊆A = ZChain.chain⊆A zc0 ; f-total = ZChain.f-total zc0 - ; f-next = {!!} - ; f-immediate = {!!} ; chain∋x = ZChain.chain∋x zc0 ; is-max = {!!} } where + ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } -- no extention + ... | no noapx = {!!} -- we have previous ordinal but ¬ A ∋ op + ind f mf x prev ya | no ¬ox with trio< (& A) x --- limit ordinal case + ... | tri< a ¬b ¬c = {!!} where zc0 = prev (& A) a ... | tri≈ ¬a b ¬c = {!!} - ... | tri> ¬a ¬b c = record { chain = uzc ; chain⊆A = record { incl = λ {x} lt → proj1 lt } ; f-total = {!!} ; f-next = {!!} - ; f-immediate = {!!} ; chain∋x = {!!} ; is-max = {!!} } where + ... | tri> ¬a ¬b c = {!!} where uzc : HOD uzc = UZFChain f mf x prev zorn00 : Maximal A @@ -443,32 +426,16 @@ 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 (zorn03 (cf nmx) (cf-is-≤-monotonic nmx))) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx zorn04) where -- if we have no maximal, make ZChain, which contradict SUP condition nmx : ¬ Maximal A nmx mx = ∅< {HasMaximal} zc5 ( ≡o∅→=od∅ ¬Maximal ) where zc5 : odef A (& (Maximal.maximal mx)) ∧ (( y : Ordinal ) → odef A y → ¬ (* (& (Maximal.maximal mx)) < * y)) zc5 = ⟪ Maximal.A∋maximal mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ - record ZChain1 ( A : HOD ) {x : Ordinal} (ax : odef A x) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) - (sup : (C : Ordinal ) → (* C ⊆ A) → IsTotalOrderSet (* C) → Ordinal) : Set (Level.suc n) where - field - chain : HOD - chain⊆A : chain ⊆ A - chain∋x : odef chain x - f-total : IsTotalOrderSet chain - f-next : {a : Ordinal } → odef chain a → odef chain (f a) - f-immediate : { x y : Ordinal } → odef chain x → odef chain y → ¬ ( ( * x < * y ) ∧ ( * y < * (f x )) ) - is-max : {a b : Ordinal } → (ca : odef chain a ) → (ba : odef A b) - → Prev< A chain ba f - ∨ (sup (& chain) (subst (λ k → k ⊆ A) (sym *iso) chain⊆A) (subst (λ k → IsTotalOrderSet k) (sym *iso) f-total) ≡ b ) - → * a < * b → odef chain b - ind4 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (x : Ordinal) → - ((y : Ordinal) → y o< x → odef A y ∧ ((ya : odef A y) → ZChain1 A ya f mf supO)) → odef A x ∧ ((ya : odef A x) → ZChain1 A ya f mf supO) - ind4 = {!!} - zorn04 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → odef A (& s) ∧ ((ya : odef A (& s)) → ZChain1 A ya f mf supO ) - zorn04 f mf = TransFinite {λ y → odef A y ∧ ( (ya : odef A y ) → ZChain1 A ya f mf supO ) } (ind4 f mf) (& s ) - zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → ZChain A sa f mf supO (& A) - zorn03 f mf = TransFinite (ind f mf) (& A) + zorn03 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → (ya : odef A (& s)) → ZChain A ya f mf supO + zorn03 f mf = TransFinite {λ y → (ya : odef A y ) → ZChain A ya f mf supO } (ind f mf) (& s ) + zorn04 : ZChain A (subst (λ k → odef A k ) &iso sa ) (cf nmx) (cf-is-≤-monotonic nmx) supO + zorn04 = zorn03 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso sa ) -- usage (see filter.agda ) --