Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/zorn.agda @ 653:4186c0331abb
sind again
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 30 Jun 2022 06:57:05 +0900 |
| parents | 75578f19ed3c |
| children | 6df8b836e983 |
line wrap: on
line diff
--- a/src/zorn.agda Sat Jun 25 17:36:18 2022 +0900 +++ b/src/zorn.agda Thu Jun 30 06:57:05 2022 +0900 @@ -230,23 +230,37 @@ x=fy : x ≡ f y record IsSup (A B : HOD) {x : Ordinal } (xa : odef A x) : Set n where - field + ield x<sup : {y : Ordinal} → odef B y → (y ≡ x ) ∨ (y << x ) -record ZChain ( A : HOD ) (x : Ordinal) ( f : Ordinal → Ordinal ) ( z : Ordinal ) : Set (Level.suc n) where +record ZChain1 ( z : Ordinal ) : Set (Level.suc n) where field supf : Ordinal → HOD + chain-mono : {x : Ordinal} → x o≤ z → supf x ⊆' supf z + +ZChain0 : (A : HOD ) → Set (Level.suc n) +ZChain0 A = ZChain1 ( & A ) + +record ZChain ( A : HOD ) (init : Ordinal) ( f : Ordinal → Ordinal ) (zc0 : ZChain0 A ) ( z : Ordinal ) : Set (Level.suc n) where chain : HOD - chain = supf z + chain = ZChain1.supf zc0 z field chain⊆A : chain ⊆' A - chain∋x : odef chain x - initial : {y : Ordinal } → odef chain y → * x ≤ * y + chain∋init : odef chain init + initial : {y : Ordinal } → odef chain y → * init ≤ * y f-next : {a : Ordinal } → odef chain a → odef chain (f a) + f-total : {x : Ordinal} → IsTotalOrderSet chain is-max : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc z → (ab : odef A b) → HasPrev A chain ab f ∨ IsSup A chain ab → * a < * b → odef chain b - pmono : (x : Ordinal ) → x o≤ z → supf x ⊆' supf z + +record UZFChain ( A : HOD ) ( f : Ordinal → Ordinal ) (zc0 : ZChain0 A ) (x y : Ordinal) + (prev : (z : Ordinal) → z o< x → ZChain A y f zc0 z) (z : Ordinal) : Set n where + -- Union of ZFChain from y which has maximality o< x + field + u : Ordinal + u<x : u o< x + chain∋z : odef (ZChain.chain (prev u u<x )) z record Maximal ( A : HOD ) : Set (Level.suc n) where field @@ -319,20 +333,21 @@ 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 ) ⟫ - sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) - sp0 f mf zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain0 A) (zc : ZChain A (& s) f zc0 (& A) ) + (total : IsTotalOrderSet (ZChain.chain zc) ) → SUP A (ZChain.chain zc) + sp0 f mf zc0 zc total = supP (ZChain.chain zc) (ZChain.chain⊆A zc) total zc< : {x y z : Ordinal} → {P : Set n} → (x o< y → P) → x o< z → z o< y → P zc< {x} {y} {z} {P} prev x<z z<y = prev (ordtrans x<z z<y) --- --- the maximum chain has fix point of any ≤-monotonic function --- - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc : ZChain A (& s) f (& A) ) + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain0 A ) (zc : ZChain A (& s) f zc0 (& A) ) → (total : IsTotalOrderSet (ZChain.chain zc) ) - → f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total)) - fixpoint f mf zc total = z14 where + → f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total)) + fixpoint f mf zc0 zc total = z14 where chain = ZChain.chain zc - sp1 = sp0 f mf zc total + sp1 = sp0 f mf zc0 zc total z10 : {a b : Ordinal } → (ca : odef chain a ) → b o< osuc (& A) → (ab : odef A b ) → HasPrev A chain ab f ∨ IsSup A chain {b} ab -- (supO chain (ZChain.chain⊆A zc) (ZChain.f-total zc) ≡ b ) → * a < * b → odef chain b @@ -341,11 +356,11 @@ z11 = c<→o< ( SUP.A∋maximal sp1) 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 ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1) + ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc ) + ... | no ne = z10 {& s} {& (SUP.sup sp1)} ( ZChain.chain∋init zc ) (ordtrans z11 <-osuc ) (SUP.A∋maximal sp1) (case2 z19 ) z13 where z13 : * (& s) < * (& (SUP.sup sp1)) - z13 with SUP.x<sup sp1 ( ZChain.chain∋x zc ) + 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.A∋maximal sp1) @@ -355,7 +370,7 @@ ... | case1 y=p = case1 (subst (λ k → k ≡ _ ) &iso ( cong (&) y=p )) ... | case2 y<p = case2 (subst (λ k → * y < k ) (sym *iso) y<p ) -- λ {y} zy → subst (λ k → (y ≡ & k ) ∨ (y << & k)) ? (SUP.x<sup sp1 ? ) } - z14 : f (& (SUP.sup (sp0 f mf zc total ))) ≡ & (SUP.sup (sp0 f mf zc total )) + z14 : f (& (SUP.sup (sp0 f mf zc0 zc total ))) ≡ & (SUP.sup (sp0 f mf zc0 zc total )) z14 with total (subst (λ k → odef chain k) (sym &iso) (ZChain.f-next zc z12 )) z12 ... | tri< a ¬b ¬c = ⊥-elim z16 where z16 : ⊥ @@ -376,92 +391,59 @@ -- 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 ) → (zc : ZChain A (& s) (cf nmx) (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥ - z04 nmx zc total = <-irr0 {* (cf nmx c)} {* c} (subst (λ k → odef A k ) (sym &iso) (proj1 (is-cf nmx (SUP.A∋maximal sp1 )))) + z04 : (nmx : ¬ Maximal A ) → (zc0 : ZChain0 A) (zc : ZChain A (& s) (cf nmx) zc0 (& A)) → IsTotalOrderSet (ZChain.chain zc) → ⊥ + z04 nmx zc0 zc total = <-irr0 {* (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 (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc total ))) -- x ≡ f x ̄ + (case1 ( cong (*)( fixpoint (cf nmx) (cf-is-≤-monotonic nmx ) zc0 zc total ))) -- x ≡ f x ̄ (proj1 (cf-is-<-monotonic nmx c (SUP.A∋maximal sp1 ))) where -- x < f x sp1 : SUP A (ZChain.chain zc) - sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc total + sp1 = sp0 (cf nmx) (cf-is-≤-monotonic nmx) zc0 zc total c = & (SUP.sup sp1) -- -- create all ZChains under o< x -- - ys : {y : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → HOD - ys {y} ay f mf = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = {!!} } - init-chain : {y x : Ordinal} → (ay : odef A y) (f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → x o< osuc y → ZChain A y f x - init-chain {y} {x} ay f mf x≤y = record { chain⊆A = λ fx → A∋fc y f mf fx - ; f-next = λ {x} sx → fsuc x sx ; supf = λ _ → ys ay f mf - ; initial = {!!} ; chain∋x = init ay ; is-max = is-max ; pmono = {!!} } where - i-total : IsTotalOrderSet (ys ay f mf ) - i-total fa fb = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp y f mf fa fb) - is-max : {a b : Ordinal} → odef (ys ay f mf) a → - b o< osuc x → (ab : odef A b) → HasPrev A (ys ay f mf) ab f ∨ IsSup A (ys ay f mf) ab → - * a < * b → odef (ys ay f mf) b - is-max {a} {b} yca b≤x ab P a<b = {!!} - initial : {i : Ordinal} → odef (ys ay f mf) i → * y ≤ * i - initial {i} (init ai) = case1 refl - initial .{f x} (fsuc x lt) = {!!} - - record ZChain0 ( A : HOD ) : Set (Level.suc n) where - field - chain : HOD - chain⊆A : chain ⊆' A - sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ((z : Ordinal) → z o< x → ZChain0 A ) → ZChain0 A + → ((z : Ordinal) → z o< x → ZChain1 z ) → ZChain1 x sind f mf {y} ay x prev with Oprev-p x ... | yes op = sc4 where px = Oprev.oprev op - sc : ZChain0 A + sc : ZChain1 px sc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) - sc4 : ZChain0 A + sc4 : ZChain1 x sc4 with ODC.∋-p O A (* x) - ... | no noax = sc - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain0.chain sc) ax f ) - ... | case1 pr = sc - ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain0.chain sc) ax ) - ... | case1 is-sup = record { chain = schain ; chain⊆A = {!!} } where + ... | no noax = ? + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.supf sc x) ax f ) + ... | case1 pr = ? + ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.supf sc x) ax ) + ... | case1 is-sup = ? where -- A∋sc -- x is a sup of zc - sup0 : SUP A (ZChain0.chain sc ) + sup0 : SUP A (ZChain1.supf sc x ) sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where - x21 : {y : HOD} → (ZChain0.chain sc) ∋ y → (y ≡ * x) ∨ (y < * x) + x21 : {y : HOD} → (ZChain1.supf sc x) ∋ y → (y ≡ * x) ∨ (y < * x) x21 {y} zy with IsSup.x<sup is-sup zy ... | case1 y=x = case1 (subst₂ (λ j k → j ≡ * k ) *iso &iso ( cong (*) y=x) ) ... | case2 y<x = case2 (subst₂ (λ j k → j < * k ) *iso &iso y<x ) sp : HOD sp = SUP.sup sup0 schain : HOD - schain = record { od = record { def = λ x → odef (ZChain0.chain sc) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!} } - ... | case2 ¬x=sup = sc - ... | no ¬ox with trio< x y - ... | tri< a ¬b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}} ; chain⊆A = {!!} } - ... | tri≈ ¬a b ¬c = record { chain = record { od = record { def = λ x → FClosure A f y x } ; odmax = & A ; <odmax = λ {y} sy → {!!}} ; chain⊆A = {!!} } - ... | tri> ¬a ¬b y<x = record { chain = Uz ; chain⊆A = {!!} } where - record Usup (z : Ordinal) : Set n where -- Union of supf from y which has maximality o< x - field - u : Ordinal - u<x : u o< x - chain∋z : odef (ZChain0.chain (prev u u<x )) z - Uz : HOD - Uz = record { od = record { def = λ y → Usup y } ; odmax = & A - ; <odmax = {!!} } -- λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) } + schain = record { od = record { def = λ x → odef (ZChain1.supf sc x) x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → {!!} } + ... | case2 ¬x=sup = ? + ... | no ¬ox = ? - - ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ((z : Ordinal) → z o< x → ZChain A y f z) → ZChain A y f x - ind f mf {y} ay x prev with Oprev-p x + ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (zc0 : ZChain0 A) → (x : Ordinal) + → ((z : Ordinal) → z o< x → ZChain A y f zc0 z) → ZChain A y f zc0 x + ind f mf {y} ay zc0 x prev with Oprev-p x ... | yes op = zc4 where -- -- we have previous ordinal to use induction -- px = Oprev.oprev op supf : Ordinal → HOD - supf = ZChain.supf (prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) ) - zc : ZChain A y f (Oprev.oprev op) + supf = ZChain1.supf zc0 + zc : ZChain A y f zc0 (Oprev.oprev op) zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) zc-b<x : (b : Ordinal ) → b o< x → b o< osuc px zc-b<x b lt = subst (λ k → b o< k ) (sym (Oprev.oprev=x op)) lt @@ -472,13 +454,13 @@ -- no-extenion : ( {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab → - * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f x - no-extenion is-max = record { supf = supf0 ; chain⊆A = subst (λ k → k ⊆' A ) seq (ZChain.chain⊆A zc) - ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) seq (ZChain.initial zc) - ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) seq (ZChain.f-next zc) - ; chain∋x = subst (λ k → odef k y ) seq (ZChain.chain∋x zc) ; pmono = {!!} + * a < * b → odef (ZChain.chain zc) b ) → ZChain A y f zc0 x + no-extenion is-max = record { supf = supf0 ; chain⊆A = subst (λ k → k ⊆' A ) ? (ZChain.chain⊆A zc) + ; initial = subst (λ k → {y₁ : Ordinal} → odef k y₁ → * y ≤ * y₁ ) ? (ZChain.initial zc) + ; f-next = subst (λ k → {a : Ordinal} → odef k a → odef k (f a) ) ? (ZChain.f-next zc) + ; chain∋init = subst (λ k → odef k y ) ? (ZChain.chain∋init zc) ; pmono = {!!} ; is-max = subst (λ k → {a b : Ordinal} → odef k a → b o< osuc x → (ab : odef A b) → - HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) seq is-max } where + HasPrev A k ab f ∨ IsSup A k ab → * a < * b → odef k b ) ? is-max } where supf0 : Ordinal → HOD supf0 z with trio< z x ... | tri< a ¬b ¬c = supf z @@ -495,7 +477,7 @@ ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) - zc4 : ZChain A y f x + zc4 : ZChain A y f zc0 x zc4 with ODC.∋-p O A (* x) ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip zc1 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → @@ -504,7 +486,7 @@ zc1 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox ... | case1 eq = ⊥-elim ( noax (subst (λ k → odef A k) (trans eq (sym &iso)) ab ) ) ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab P a<b - ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf supO x + ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain.chain zc) ax f ) -- we have to check adding x preserve is-max ZChain A y f mf zc0 x ... | case1 pr = no-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next chain0 = ZChain.chain zc zc7 : {a b : Ordinal} → odef (ZChain.chain zc) a → b o< osuc x → (ab : odef A b) → @@ -516,7 +498,7 @@ ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax ) ... | case1 is-sup = -- x is a sup of zc record { chain⊆A = {!!} ; f-next = {!!} ; pmono = {!!} - ; initial = {!!} ; chain∋x = {!!} ; is-max = {!!} ; supf = supf0 } where + ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} ; supf = supf0 } where sup0 : SUP A (ZChain.chain zc) sup0 = record { sup = * x ; A∋maximal = ax ; x<sup = x21 } where x21 : {y : HOD} → ZChain.chain zc ∋ y → (y ≡ * x) ∨ (y < * x) @@ -571,7 +553,7 @@ scnext {x} (case2 sx) = case2 ( fsuc x sx ) scinit : {x : Ordinal} → odef schain x → * y ≤ * x scinit {x} (case1 zx) = ZChain.initial zc zx - scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋x zc ) ) + scinit {x} (case2 sx) with (s≤fc (& sp) f mf sx ) | SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) ( ZChain.chain∋init zc ) ) ... | case1 sp=x | case1 y=sp = case1 (trans y=sp (subst (λ k → k ≡ * x ) *iso sp=x ) ) ... | case1 sp=x | case2 y<sp = case2 (subst (λ k → * y < k ) (trans (sym *iso) sp=x) y<sp ) ... | case2 sp<x | case1 y=sp = case2 (subst (λ k → k < * x ) (trans *iso (sym y=sp )) sp<x ) @@ -600,9 +582,9 @@ z24 : IsSup A schain ab → IsSup A (ZChain.chain zc) ab z24 p = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } z23 : odef chain0 b - z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋x zc ) - ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋x zc ) - ... | case2 y<b = ZChain.is-max zc (ZChain.chain∋x zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b + z23 with IsSup.x<sup (z24 p) ( ZChain.chain∋init zc ) + ... | case1 y=b = subst (λ k → odef chain0 k ) y=b ( ZChain.chain∋init zc ) + ... | case2 y<b = ZChain.is-max zc (ZChain.chain∋init zc ) (zc-b<x b b<x) ab (case2 (z24 p)) y<b seq : schain ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) @@ -624,32 +606,30 @@ ... | case1 pr = ⊥-elim ( ¬fy<x record {y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = trans (trans &iso (sym b=x) ) (HasPrev.x=fy pr ) } ) ... | case2 b=sup = ⊥-elim ( ¬x=sup record { x<sup = λ {y} zy → subst (λ k → (y ≡ k) ∨ (y << k)) (trans b=x (sym &iso)) (IsSup.x<sup b=sup zy) } ) - ... | no ¬ox with trio< x y - ... | tri< a ¬b ¬c = init-chain ay f mf {!!} - ... | tri≈ ¬a b ¬c = init-chain ay f mf {!!} - ... | tri> ¬a ¬b y<x = record { supf = supf0 ; chain⊆A = {!!} ; f-next = {!!} ; pmono = {!!} - ; initial = {!!} ; chain∋x = {!!} ; is-max = {!!} } where --- limit ordinal case - record UZFChain (z : Ordinal) : Set n where -- Union of ZFChain from y which has maximality o< x - field - u : Ordinal - u<x : u o< x - chain∋z : odef (ZChain.chain (prev u u<x )) z - Uz⊆A : {z : Ordinal} → UZFChain z → odef A z - Uz⊆A {z} u = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u) - uzc : {z : Ordinal} → (u : UZFChain z) → ZChain A y f (UZFChain.u u) + ... | no ¬ox = record { chain⊆A = ? ; f-next = ? ; chain = ? + ; initial = ? ; chain∋init = ? ; is-max = {!!} } where --- limit ordinal case + supf : Ordinal → HOD + supf = ZChain1.supf zc0 + Uz⊆A : {z : Ordinal} → UZFChain A f zc0 x y prev z ∨ FClosure A f y z → odef A z + Uz⊆A {z} (case1 u) = ZChain.chain⊆A ( prev (UZFChain.u u) (UZFChain.u<x u) ) (UZFChain.chain∋z u) + Uz⊆A (case2 lt) = A∋fc _ f mf lt + uzc : {z : Ordinal} → (u : UZFChain A f zc0 x y prev z) → ZChain A y f zc0 (UZFChain.u u) uzc {z} u = prev (UZFChain.u u) (UZFChain.u<x u) Uz : HOD - Uz = record { od = record { def = λ y → UZFChain y } ; odmax = & A + Uz = record { od = record { def = λ z → UZFChain A f zc0 x y prev z ∨ FClosure A f y z } ; odmax = & A ; <odmax = λ lt → subst (λ k → k o< & A ) &iso (c<→o< (subst (λ k → odef A k ) (sym &iso) (Uz⊆A lt))) } u-next : {z : Ordinal} → odef Uz z → odef Uz (f z) - u-next {z} u = record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u) } + u-next {z} (case1 u) = case1 record { u = UZFChain.u u ; u<x = UZFChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UZFChain.chain∋z u) } + u-next {z} (case2 u) = case2 ( fsuc _ u ) u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z - u-initial {z} u = ZChain.initial ( uzc u ) (UZFChain.chain∋z u) - u-chain∋x : odef Uz y - u-chain∋x = record { u = y ; u<x = y<x ; chain∋z = ZChain.chain∋x (prev y y<x ) } + u-initial {z} (case1 u) = ZChain.initial ( uzc u ) (UZFChain.chain∋z u) + u-initial {z} (case2 u) = s≤fc _ f mf u + u-chain∋init : odef Uz y + u-chain∋init = case2 ( init ay ) + supf0 : Ordinal → HOD supf0 z with trio< z x - ... | tri< a ¬b ¬c = ZChain.supf (prev z a ) z + ... | tri< a ¬b ¬c = ZChain1.supf zc0 z ... | tri≈ ¬a b ¬c = Uz ... | tri> ¬a ¬b c = Uz seq : Uz ≡ supf0 x @@ -657,52 +637,21 @@ ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = refl - seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain.supf (prev b b<x ) b ≡ supf0 b + seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain1.supf zc0 b ≡ supf0 b seq<x {b} b<x with trio< b x - ... | tri< a ¬b ¬c = cong (λ k → ZChain.supf (prev b k ) b) o<-irr -- b<x ≡ a + ... | tri< a ¬b ¬c = cong (λ k → ZChain1.supf zc0 b) o<-irr -- b<x ≡ a ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) ord≤< : {x y z : Ordinal} → x o< z → z o≤ y → x o< y ord≤< {x} {y} {z} x<z z≤y with osuc-≡< z≤y ... | case1 z=y = subst (λ k → x o< k ) z=y x<z ... | case2 z<y = ordtrans x<z z<y - u-mono : {z : Ordinal} → z o≤ x → supf0 z ⊆' supf0 x - u-mono {z} z≤x {i} with trio< z x | trio< x x - ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = λ lt → {!!} - ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = λ lt → record { u = {!!} ; u<x = {!!} ; chain∋z = lt } - ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = λ lt → {!!} - ... | tri≈ ¬a b ¬c | s = {!!} -- λ lt → lt - ... | tri> ¬a ¬b c | s = {!!} -- λ lt → lt - SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (& A) - SZ f mf {y} ay = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) (& A) - - postulate - TFcomm : { ψ : Ordinal → Set (Level.suc n) } - → (ind : (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x ) - → ∀ (x : Ordinal) → ind x (λ y _ → TransFinite ind y ) ≡ TransFinite ind x + SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain0 A + SZ0 f mf ay = TransFinite {λ z → ZChain1 z} (sind f mf ay ) (& A) - record ZChain1 ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) : Set (Level.suc n) where - field - zc : ZChain A y f (& A) - supf = ZChain.supf zc - field - chain-mono : {x y : Ordinal} → x o≤ y → supf x ⊆' supf y - f-total : {x : Ordinal} → IsTotalOrderSet (supf x) - - SZ1 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} → (ay : odef A y) - → ZChain1 f mf ay - SZ1 f mf {y} ay = record { zc = TransFinite {λ z → ZChain A y f z } (ind f mf ay ) (& A) - ; chain-mono = mono sf ; f-total = {!!} } where -- TransFinite {λ w → ZChain1 f mf ay w} indp z where - sf : Ordinal → HOD - sf x = ZChain.supf (TransFinite (ind f mf ay) (& A)) x - sf' : Ordinal → HOD - sf' x = ZChain.supf (ind f mf ay (& A) {!!} ) x - mono : {x : Ordinal} {w : Ordinal} (sf : Ordinal → HOD) → x o≤ w → sf x ⊆' sf w - mono {a} {b} sf a≤b = TransFinite0 {λ b → a o≤ b → sf a ⊆' sf b } mind b a≤b where - mind : (x : Ordinal) → ((y₁ : Ordinal) → y₁ o< x → a o≤ y₁ → sf a ⊆' sf y₁) → a o≤ x → sf a ⊆' sf x - mind x prev a≤x sai = {!!} - + SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ya : odef A y) → ZChain A y f (SZ0 f mf ya) (& A) + SZ f mf {y} ay = TransFinite {λ z → ZChain A y f (SZ0 f mf ay) z } (ind f mf ay (SZ0 f mf ay) ) (& A) zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM @@ -714,16 +663,18 @@ 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 zorn04 total ) where + ... | yes ¬Maximal = ⊥-elim ( z04 nmx zc0 zorn04 total ) 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) ) ⟫ - zorn04 : ZChain A (& s) (cf nmx) (& A) - zorn04 = ZChain1.zc ( SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) ) + zc0 : ZChain0 A + zc0 = TransFinite {λ z → ZChain1 z} (sind (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as )) (& A) + zorn04 : ZChain A (& s) (cf nmx) zc0 (& A) + zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) total : IsTotalOrderSet (ZChain.chain zorn04) - total = ZChain1.f-total (SZ1 (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) + total = ZChain.f-total (SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as) ) -- usage (see filter.agda ) --