Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 674:a48845e246e4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 09 Jul 2022 11:16:57 +0900 |
| parents | 79616ba278c0 |
| children | 6a9a98904f7a |
| files | src/OrdUtil.agda src/zorn.agda |
| diffstat | 2 files changed, 102 insertions(+), 115 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OrdUtil.agda Fri Jul 08 17:42:29 2022 +0900 +++ b/src/OrdUtil.agda Sat Jul 09 11:16:57 2022 +0900 @@ -167,6 +167,12 @@ o≤-refl : { i : Ordinal } → i o≤ i o≤-refl {i} = subst (λ k → i o< osuc k ) refl <-osuc +o≤? : (x y : Ordinal) → Dec ( x o≤ y ) +o≤? x y with trio< x y +... | tri< a ¬b ¬c = yes (ordtrans a <-osuc) +... | tri≈ ¬a b ¬c = yes (o≤-refl0 b) +... | tri> ¬a ¬b c = no (λ n → osuc-< n c ) + OrdTrans : Transitive _o≤_ OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
--- a/src/zorn.agda Fri Jul 08 17:42:29 2022 +0900 +++ b/src/zorn.agda Sat Jul 09 11:16:57 2022 +0900 @@ -262,17 +262,20 @@ field psup : Ordinal p≤z : psup o≤ z - pchain : {px : Ordinal} → px o≤ z → (w : Ordinal) → Chain A f mf ay px w - chain-mono : (px : Ordinal) → (x≤p : px o≤ psup ) → (w : Ordinal ) → Chain A f mf ay px w → Chain A f mf ay psup w + chainf : {px : Ordinal} → px o≤ z → (w : Ordinal) → Chain A f mf ay px w + chain-mono1 : (px : Ordinal) → (x≤p : px o≤ psup ) → (w : Ordinal ) → Chain A f mf ay px w → Chain A f mf ay psup w ChainF : (A : HOD) → ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) → (z : Ordinal) → ZChain1 A f mf ay (& A) → HOD ChainF A f mf {y} ay z zc = record { od = record { def = λ x → odef A x ∧ Chain A f mf ay (ZChain1.psup zc) x } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } -record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) (zc0 : ZChain1 A f mf ay (& A) ) ( z : Ordinal ) : Set (Level.suc n) where +record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) + (zc0 : (x : Ordinal) → ZChain1 A f mf ay x ) ( z : Ordinal ) : Set (Level.suc n) where chain : HOD - chain = ChainF A f mf ay z zc0 + chain = ChainF A f mf ay z (zc0 (& A)) field + chain-mono : (px py : Ordinal) → (px≤py : px o≤ py ) (y≤x : py o≤ z ) → (w : Ordinal ) + → Chain A f mf ay (ZChain1.psup (zc0 (& A))) px → Chain A f mf ay (ZChain1.psup (zc0 (& A))) py chain⊆A : chain ⊆' A chain∋init : odef chain init initial : {y : Ordinal } → odef chain y → * init ≤ * y @@ -345,7 +348,7 @@ 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 ) (zc0 : ZChain1 A f mf as0 (& A) ) (zc : ZChain A f mf as0 zc0 (& A) ) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : (x : Ordinal) → ZChain1 A f mf as0 x ) (zc : ZChain A f mf as0 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 @@ -354,7 +357,7 @@ --- --- the maximum chain has fix point of any ≤-monotonic function --- - fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A)) (zc : ZChain A f mf as0 zc0 (& A) ) + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : (x : Ordinal) → ZChain1 A f mf as0 x) (zc : ZChain A f mf as0 zc0 (& A) ) → (total : IsTotalOrderSet (ZChain.chain zc) ) → 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 @@ -403,7 +406,7 @@ -- 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 ) → (zc0 : ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 zc0 (& A)) + z04 : (nmx : ¬ Maximal A ) → (zc0 : (x : Ordinal) → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx) as0 x) (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 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) ) @@ -464,46 +467,59 @@ ... | case1 is-sup = ? ... | case2 ¬x=sup = ? - ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) → (zc0 : ZChain1 A f mf ay (& A)) + ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) + → (zc0 : (x : Ordinal) → ZChain1 A f mf ay x) → ((z : Ordinal) → z o< x → ZChain A f mf ay zc0 z) → ZChain A f mf ay zc0 x - ind f mf {y} ay x zc0 prev with Oprev-p x - ... | yes op = zc4 where - -- - -- we have previous ordinal to use induction - -- - px = Oprev.oprev op - supf : Ordinal → HOD - supf x = ? -- ZChain1.chain zc0 - zc : ZChain A f mf ay 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 - px<x : px o< x - px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc + ind f mf {y} ay x zc0 prev = zc4 where + zc : {z1 : Ordinal} → z1 o< x → ZChain A f mf ay zc0 z1 + zc z1 with Oprev-p x + ... | yes op = ? where + -- + -- we have previous ordinal to use induction + -- + px = Oprev.oprev op + supf : Ordinal → HOD + supf x = ChainF A f mf ay x (zc0 (& A)) + -- zc : ZChain A f mf ay zc0 (Oprev.oprev op) + -- zc = prev px (subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc ) + px<x : px o< x + px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc + ... | no ¬ox = ? where + supf : Ordinal → HOD + supf x = ? -- Z?Chain1.chain zc0 + uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf ay zc0 (UChain.u u) + uzc {z} u = prev (UChain.u u) (UChain.u<x u) + Uz : HOD + Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!} } -- if previous chain satisfies maximality, we caan reuse it -- - 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 f mf ay {!!} x - no-extenion is-max = record { 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) - ; f-total = {!!} - ; chain∋init = subst (λ k → odef k y ) {!!} (ZChain.chain∋init zc) - ; 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 ) {!!} is-max } where + 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 f mf ay zc0 x + no-extenion is-max with o≤? x (& A) + ... | no n = ? where + ... | yes x≤a with ZChain1.chainf (zc0 (& A)) x≤a x + ... | ch-init _ _ x=0 fc = ? + ... | ch-is-sup ax is-sup fc = ? where + -- = record { 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) + -- ; f-total = {!!} + -- ; chain∋init = subst (λ k → odef k y ) {!!} (ZChain.chain∋init zc) + -- ; 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 ) {!!} is-max } where supf0 : Ordinal → HOD supf0 z with trio< z x - ... | tri< a ¬b ¬c = supf z - ... | tri≈ ¬a b ¬c = ZChain.chain zc - ... | tri> ¬a ¬b c = ZChain.chain zc - seq : ZChain.chain zc ≡ supf0 x + ... | tri< a ¬b ¬c = ? + ... | tri≈ ¬a b ¬c = ZChain.chain (zc ?) + ... | tri> ¬a ¬b c = ZChain.chain (zc ?) + seq : ZChain.chain (zc ?) ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = refl - seq<x : {b : Ordinal } → b o< x → supf b ≡ supf0 b + seq<x : {b : Ordinal } → b o< x → ? -- supf b ≡ supf0 b seq<x {b} b<x with trio< b x ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) @@ -512,28 +528,29 @@ zc4 : ZChain A f mf ay 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) → - HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab → - * a < * b → odef (ZChain.chain zc) b + zc1 : {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 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 zc0 x + ... | case2 lt = ZChain.is-max (zc ?) za ? 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 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) → - HasPrev A (ZChain.chain zc) ab f ∨ IsSup A (ZChain.chain zc) ab → - * a < * b → odef (ZChain.chain zc) b + chain0 = ZChain.chain (zc ?) + zc7 : {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 zc7 {a} {b} za b<ox ab P a<b with osuc-≡< b<ox - ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab P a<b - ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next zc (HasPrev.ay pr)) - ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain.chain zc) ax ) - ... | case1 is-sup = -- x is a sup of zc + ... | case2 lt = ZChain.is-max (zc ?) za ? ab P a<b + ... | case1 b=x = subst (λ k → odef chain0 k ) (trans (sym (HasPrev.x=fy pr )) (trans &iso (sym b=x)) ) ( ZChain.f-next (zc ?) (HasPrev.ay pr)) + ... | 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 = {!!} ; f-total = {!!} ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where - sup0 : SUP A (ZChain.chain zc) + 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) + x21 : {y : HOD} → ZChain.chain (zc ?) ∋ 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 ) @@ -541,22 +558,22 @@ sp = SUP.sup sup0 x=sup : x ≡ & sp x=sup = sym &iso - chain0 = ZChain.chain zc + chain0 = ZChain.chain (zc ?) sc<A : {y : Ordinal} → odef chain0 y ∨ FClosure A f (& sp) y → y o< & A - sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A zc (subst (λ k → odef chain0 k) (sym &iso) zx ))) + sc<A {y} (case1 zx) = subst (λ k → k o< (& A)) &iso ( c<→o< (ZChain.chain⊆A (zc ?) (subst (λ k → odef chain0 k) (sym &iso) zx ))) sc<A {y} (case2 fx) = subst (λ k → k o< (& A)) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso) (A∋fc (& sp) f mf fx )) ) schain : HOD schain = record { od = record { def = λ x → odef chain0 x ∨ (FClosure A f (& sp) x) } ; odmax = & A ; <odmax = λ {y} sy → sc<A {y} sy } supf0 : Ordinal → HOD supf0 z with trio< z x - ... | tri< a ¬b ¬c = supf z + ... | tri< a ¬b ¬c = ? -- supf z ... | tri≈ ¬a b ¬c = schain ... | tri> ¬a ¬b c = schain A∋schain : {x : HOD } → schain ∋ x → A ∋ x - A∋schain (case1 zx ) = ZChain.chain⊆A zc zx + A∋schain (case1 zx ) = ZChain.chain⊆A (zc ?) zx A∋schain {y} (case2 fx ) = A∋fc (& sp) f mf fx s⊆A : schain ⊆' A - s⊆A {x} (case1 zx) = ZChain.chain⊆A zc zx + s⊆A {x} (case1 zx) = ZChain.chain⊆A (zc ?) zx s⊆A {x} (case2 fx) = A∋fc (& sp) f mf fx cmp : {a b : HOD} (za : odef chain0 (& a)) (fb : FClosure A f (& sp) (& b)) → Tri (a < b) (a ≡ b) (b < a ) cmp {a} {b} za fb with SUP.x<sup sup0 za | s≤fc (& sp) f mf fb @@ -573,7 +590,7 @@ a<b : a < b a<b = ptrans (subst (λ k → a < k ) (sym *iso) a<sp ) ( subst₂ (λ j k → j < k ) refl *iso sp<b ) scmp : {a b : HOD} → odef schain (& a) → odef schain (& b) → Tri (a < b) (a ≡ b) (b < a ) - scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total zc {px} {px} o≤-refl za zb + scmp {a} {b} (case1 za) (case1 zb) = {!!} -- ZChain.f-total (zc ?) {px} {px} o≤-refl za zb scmp {a} {b} (case1 za) (case2 fb) = cmp za fb scmp (case2 fa) (case1 zb) with cmp zb fa ... | tri< a ¬b ¬c = tri> ¬c (λ eq → ¬b (sym eq)) a @@ -581,17 +598,17 @@ ... | tri> ¬a ¬b c = tri< c (λ eq → ¬b (sym eq)) ¬a scmp (case2 fa) (case2 fb) = subst₂ (λ a b → Tri (a < b) (a ≡ b) (b < a ) ) *iso *iso (fcn-cmp (& sp) f mf fa fb) scnext : {a : Ordinal} → odef schain a → odef schain (f a) - scnext {x} (case1 zx) = case1 (ZChain.f-next zc zx) + scnext {x} (case1 zx) = case1 (ZChain.f-next (zc ?) zx) 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∋init zc ) ) + 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∋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 ) ... | case2 sp<x | case2 y<sp = case2 (ptrans y<sp (subst (λ k → k < * x ) *iso sp<x) ) A∋za : {a : Ordinal } → odef chain0 a → odef A a - A∋za za = ZChain.chain⊆A zc za + A∋za za = ZChain.chain⊆A (zc ?) za za<sup : {a : Ordinal } → odef chain0 a → ( * a ≡ sp ) ∨ ( * a < sp ) za<sup za = SUP.x<sup sup0 (subst (λ k → odef chain0 k ) (sym &iso) za ) s-ismax : {a b : Ordinal} → odef schain a → b o< osuc x → (ab : odef A b) @@ -602,84 +619,48 @@ s-ismax {a} {b} (case1 za) b<ox ab (case1 p) a<b | case2 b<x = z21 p where -- has previous z21 : HasPrev A schain ab f → odef schain b z21 record { y = y ; ay = (case1 zy) ; x=fy = x=fy } = - case1 (ZChain.is-max zc za (zc-b<x b b<x) ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b ) + case1 (ZChain.is-max (zc ?) za ? ab (case1 record { y = y ; ay = zy ; x=fy = x=fy }) a<b ) z21 record { y = y ; ay = (case2 sy) ; x=fy = x=fy } = subst (λ k → odef schain k) (sym x=fy) (case2 (fsuc y sy) ) - s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max zc za (zc-b<x b b<x) ab (case2 z22) a<b ) where -- previous sup - z22 : IsSup A (ZChain.chain zc) ab + s-ismax {a} {b} (case1 za) b<ox ab (case2 p) a<b | case2 b<x = case1 (ZChain.is-max (zc ?) za ? ab (case2 z22) a<b ) where -- previous sup + z22 : IsSup A (ZChain.chain (zc ?) ) ab z22 = record { x<sup = λ {y} zy → IsSup.x<sup p (case1 zy ) } s-ismax {a} {b} (case2 sa) b<ox ab (case1 p) a<b | case2 b<x with HasPrev.ay p - ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next zc zy )) -- in previous closure of f + ... | case1 zy = case1 (subst (λ k → odef chain0 k ) (sym (HasPrev.x=fy p)) (ZChain.f-next (zc ?) zy )) -- in previous closure of f ... | case2 sy = case2 (subst (λ k → FClosure A f (& (* x)) k ) (sym (HasPrev.x=fy p)) (fsuc (HasPrev.y p) sy )) -- in current closure of f s-ismax {a} {b} (case2 sa) b<ox ab (case2 p) a<b | case2 b<x = case1 z23 where -- sup o< x is already in zc - z24 : IsSup A schain ab → IsSup A (ZChain.chain zc) ab + 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∋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 + 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 ?) ) ? ab (case2 (z24 p)) y<b seq : schain ≡ supf0 x seq with trio< x x ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) ... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = refl - seq<x : {b : Ordinal } → b o< x → supf b ≡ supf0 b + seq<x : {b : Ordinal } → b o< x → ? -- supf b ≡ supf0 b seq<x {b} b<x with trio< b x ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b₁ ¬c = ⊥-elim (¬a b<x ) ... | tri> ¬a ¬b c = ⊥-elim (¬a b<x ) ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention - z18 : {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 + z18 : {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 z18 {a} {b} za b<x ab p a<b with osuc-≡< b<x - ... | case2 lt = ZChain.is-max zc za (zc-b<x b lt) ab p a<b + ... | case2 lt = ZChain.is-max (zc ?) za ? ab p a<b ... | case1 b=x with p ... | 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 = record { chain⊆A = {!!} ; f-next = {!!} ; f-total = {!!} - ; initial = {!!} ; chain∋init = {!!} ; is-max = {!!} } where --- limit ordinal case - supf : Ordinal → HOD - supf x = ? -- Z?Chain1.chain zc0 - uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf ay zc0 (UChain.u u) - uzc {z} u = prev (UChain.u u) (UChain.u<x u) - Uz : HOD - Uz = record { od = record { def = λ z → odef A z ∧ ( UChain z {!!} x ∨ FClosure A f y z ) } ; odmax = & A ; <odmax = {!!} } - u-next : {z : Ordinal} → odef Uz z → odef Uz (f z) - u-next {z} = {!!} - -- (case1 u) = case1 record { u = UChain.u u ; u<x = UChain.u<x u ; chain∋z = ZChain.f-next ( uzc u ) (UChain.chain∋z u) } - -- u-next {z} (case2 u) = case2 ( fsuc _ u ) - u-initial : {z : Ordinal} → odef Uz z → * y ≤ * z - u-initial {z} = {!!} - -- (case1 u) = ZChain.initial ( uzc u ) (UChain.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 = ? -- ZChain1.chain zc0 - ... | tri≈ ¬a b ¬c = Uz - ... | tri> ¬a ¬b c = Uz - u-mono : {z : Ordinal} {w : Ordinal} → z o≤ w → w o≤ x → supf0 z ⊆' supf0 w - u-mono {z} {w} z≤w w≤x {i} with trio< z x | trio< w x - ... | s | t = {!!} - - seq : Uz ≡ supf0 x - seq with trio< x x - ... | tri< a ¬b ¬c = ⊥-elim ( ¬b refl ) - ... | tri≈ ¬a b ¬c = refl - ... | tri> ¬a ¬b c = refl - 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 SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z} (sind f mf ay ) x - SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (SZ0 f mf ay (& A)) (& A) - SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay (SZ0 f mf ay (& A)) z } (λ x → ind f mf ay x (SZ0 f mf ay (& A)) ) (& A) + SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (SZ0 f mf ay ) (& A) + SZ f mf {y} ay = TransFinite {λ z → ZChain A f mf ay (SZ0 f mf ay ) z } (λ x → ind f mf ay x (SZ0 f mf ay ) ) (& A) zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM @@ -691,7 +672,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 (zc0 (& A)) 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 @@ -699,7 +680,7 @@ 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) ) ⟫ zc0 : (x : Ordinal) → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx) as0 x zc0 x = TransFinite {λ z → ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx) as0 z} (sind (cf nmx) (cf-is-≤-monotonic nmx) as0) x - zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (zc0 (& A)) (& A) + zorn04 : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 zc0 (& A) zorn04 = SZ (cf nmx) (cf-is-≤-monotonic nmx) (subst (λ k → odef A k ) &iso as ) total : IsTotalOrderSet (ZChain.chain zorn04) total {a} {b} = zorn06 where