Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 666:431d074311f5
do all in sind
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 04 Jul 2022 21:25:38 +0900 |
| parents | 1002866230b8 |
| children | c6cd972b468c |
| files | src/zorn.agda |
| diffstat | 1 files changed, 71 insertions(+), 99 deletions(-) [+] |
line wrap: on
line diff
--- a/src/zorn.agda Mon Jul 04 07:41:30 2022 +0900 +++ b/src/zorn.agda Mon Jul 04 21:25:38 2022 +0900 @@ -254,7 +254,7 @@ UnionCF A x chainf = record { od = record { def = λ z → odef A z ∧ UChain x chainf z } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } data Chain (A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {y : Ordinal} (ay : odef A y) : Ordinal → HOD → Set (Level.suc n) where - ch-init : Chain A f mf ay o∅ record { od = record { def = λ z → FClosure A f y z } ; odmax = & A ; <odmax = λ {y} sy → ? } + ch-init : (x : Ordinal) → x ≡ o∅ → Chain A f mf ay x record { od = record { def = λ z → FClosure A f y z } ; odmax = & A ; <odmax = λ {y} sy → ? } ch-noax : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (noax : ¬ odef A x ) (c : Chain A f mf ay (Oprev.oprev op) chain) → Chain A f mf ay x chain ch-hasprev : {x : Ordinal } { chain : HOD } ( op : Oprev Ordinal osuc x ) (ax : odef A x ) ( c : Chain A f mf ay (Oprev.oprev op) chain) ( h : HasPrev A chain ax f ) → Chain A f mf ay x chain @@ -289,10 +289,9 @@ chain : HOD chain-uniq : Chain A f mf ay z chain -record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) ( z : Ordinal ) (zc0 : ZChain1 A f mf ay z ) : Set (Level.suc n) where - chain : HOD - chain = ZChain1.chain zc0 +record ZChain ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) {init : Ordinal} (ay : odef A init) ( z : Ordinal ) : Set (Level.suc n) where field + chain : HOD chain⊆A : chain ⊆' A chain∋init : odef chain init initial : {y : Ordinal } → odef chain y → * init ≤ * y @@ -365,7 +364,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 (& A) zc0 ) + sp0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A) ) (zc : ZChain A f mf as0 (& 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 @@ -374,7 +373,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 (& A) zc0 ) + fixpoint : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) (zc0 : ZChain1 A f mf as0 (& A)) (zc : ZChain A f mf as0 (& 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 @@ -423,7 +422,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 (& A) zc0 ) + 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 (& 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) ) @@ -438,25 +437,25 @@ -- sind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ((z : Ordinal) → z o< x → ZChain1 A f mf ay z ) → ZChain1 A f mf ay x + → ((z : Ordinal) → z o< x → ZChain1 A f mf ay z ∧ ZChain A f mf ay z ) → ZChain1 A f mf ay x ∧ ZChain A f mf ay x sind f mf {y} ay x prev with Oprev-p x ... | yes op = sc4 where open ZChain1 px = Oprev.oprev op px<x : px o< x px<x = subst (λ k → px o< k) (Oprev.oprev=x op) <-osuc - sc : ZChain1 A f mf ay px - sc = prev px px<x - sc4 : ZChain1 A f mf ay x + sc : ZChain1 A f mf ay px + sc = proj1 (prev px px<x) + sc4 : ZChain1 A f mf ay x ∧ ZChain A f mf ay x sc4 with ODC.∋-p O A (* x) - ... | no noax = record { chain = chain sc ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc ) } + ... | no noax = ⟪ record { chain = chain sc ; chain-uniq = ch-noax op (subst (λ k → ¬ odef A k) &iso noax) ( chain-uniq sc ) } , ? ⟫ ... | yes ax with ODC.p∨¬p O ( HasPrev A (ZChain1.chain sc ) ax f ) - ... | case1 pr = record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) - record { y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = sc6 } } where + ... | case1 pr = ⟪ record { chain = chain sc ; chain-uniq = ch-hasprev op (subst (λ k → odef A k) &iso ax) ( chain-uniq sc ) + record { y = HasPrev.y pr ; ay = HasPrev.ay pr ; x=fy = sc6 } } , ? ⟫ where sc6 : x ≡ f (HasPrev.y pr) sc6 = subst (λ k → k ≡ f (HasPrev.y pr) ) &iso ( HasPrev.x=fy pr ) ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (ZChain1.chain sc ) ax ) - ... | case1 is-sup = record { chain = schain ; chain-uniq = sc9 } where + ... | case1 is-sup = ⟪ record { chain = schain ; chain-uniq = sc9 } , ? ⟫ where schain : HOD schain = record { od = record { def = λ z → odef A z ∧ ( odef (ZChain1.chain sc ) z ∨ (FClosure A f x z)) } ; odmax = & A ; <odmax = λ {y} sy → ∈∧P→o< sy } @@ -465,27 +464,27 @@ sc9 : Chain A f mf ay x schain sc9 = ch-is-sup op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc7 record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k )) &iso (IsSup.x<sup is-sup lt) } - ... | case2 ¬x=sup = record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } where + ... | case2 ¬x=sup = ⟪ record { chain = chain sc ; chain-uniq = ch-skip op (subst (λ k → odef A k) &iso ax) (ZChain1.chain-uniq sc) sc17 sc10 } , ? ⟫ where sc17 : ¬ HasPrev A (chain sc) (subst (λ k → odef A k) &iso ax) f sc17 not = ¬fy<x record { y = HasPrev.y not ; ay = HasPrev.ay not ; x=fy = subst (λ k → k ≡ _) (sym &iso) (HasPrev.x=fy not ) } sc10 : ¬ IsSup A (chain sc) (subst (λ k → odef A k) &iso ax) sc10 not = ¬x=sup ( record { x<sup = λ {z} lt → subst (λ k → (z ≡ k ) ∨ (z << k ) ) (sym &iso) ( IsSup.x<sup not lt ) } ) ... | no ¬ox = sc4 where chainf : (z : Ordinal) → z o< x → HOD - chainf z z<x = ZChain1.chain ( prev z z<x ) + chainf z z<x = ZChain1.chain ( proj1 (prev z z<x ) ) chainq : ( z : Ordinal ) → (z<x : z o< x ) → Chain A f mf ay z ( chainf z z<x ) - chainq z z<x = ZChain1.chain-uniq ( prev z z<x) - sc4 : ZChain1 A f mf ay x + chainq z z<x = ZChain1.chain-uniq ( proj1 ( prev z z<x) ) + sc4 : ZChain1 A f mf ay x ∧ ZChain A f mf ay x sc4 with ODC.∋-p O A (* x) - ... | no noax = record { chain = UnionCF A x chainf ; chain-uniq = ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ? ? } + ... | no noax = ⟪ record { chain = UnionCF A x chainf ; chain-uniq = ch-noax-union ¬ox (subst (λ k → ¬ odef A k) &iso noax) ? ? } , ? ⟫ ... | yes ax with ODC.p∨¬p O ( HasPrev A (UnionCF A x chainf) ax f ) - ... | case1 pr = record { chain = UnionCF A x chainf ; chain-uniq = ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? ? } + ... | case1 pr = ⟪ record { chain = UnionCF A x chainf ; chain-uniq = ch-hasprev-union ¬ox (subst (λ k → odef A k) &iso ax) ? ? ? } , ? ⟫ ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A (UnionCF A x chainf) ax ) ... | case1 is-sup = ? ... | case2 ¬x=sup = ? ind : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → (x : Ordinal) - → ((z : Ordinal) → z o< x → (zc1 : ZChain1 A f mf ay z) → ZChain A f mf ay z zc1 ) → (zc0 : ZChain1 A f mf ay x ) → ZChain A f mf ay x zc0 + → ((z : Ordinal) → z o< x → (zc1 : ZChain1 A f mf ay z) → ZChain A f mf ay z ) → (zc0 : ZChain1 A f mf ay x ) → ZChain A f mf ay x ind f mf {y} ay x prev zc0 with Oprev-p x ... | yes op = zc4 where -- @@ -494,7 +493,7 @@ px = Oprev.oprev op supf : Ordinal → HOD supf x = ZChain1.chain zc0 - zc : ZChain A f mf ay (Oprev.oprev op) ? + zc : ZChain A f mf ay (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 @@ -503,35 +502,10 @@ -- 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 - 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 - 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} 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 ) - zc4 : ZChain A f mf ay x zc0 + zc4 : ZChain A f mf ay x zc4 with ODC.∋-p O A (* x) - ... | no noax = no-extenion zc1 where -- ¬ A ∋ p, just skip + ... | no noax = ? 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 @@ -539,7 +513,7 @@ ... | 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 - ... | case1 pr = no-extenion zc7 where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next + ... | case1 pr = ? 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 → @@ -646,9 +620,9 @@ 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 ) + ... | tri> ¬a ¬b c = ? -- ⊥-elim (¬a b<x zc0 ) - ... | case2 ¬x=sup = no-extenion z18 where -- x is not f y' nor sup of former ZChain from y -- no extention + ... | case2 ¬x=sup = ? 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 @@ -658,53 +632,51 @@ ... | 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 = ZChain1.chain zc0 - uzc : {z : Ordinal} → (u : UChain x {!!} z) → ZChain A f mf ay (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 = {!!} + ... | no ¬ox = zc5 where --- limit ordinal case + chainf : (zc : ZChain1 A f mf ay x ) → (z : Ordinal) → z o< x → HOD + chainf zc z z<x = ? + uzc : HOD + uzc = UnionCF A x (chainf zc0) + zc5 : ZChain A f mf ay x + zc5 with ODC.∋-p O A (* x) + ... | no noax = ? where -- ¬ A ∋ p, just skip + ... | yes ax with ODC.p∨¬p O ( HasPrev A uzc ax f ) -- we have to check adding x preserve is-max ZChain A y f mf zc0 x + ... | case1 pr = ? where -- we have previous A ∋ z < x , f z ≡ x, so chain ∋ f z ≡ x because of f-next + ... | case2 ¬fy<x with ODC.p∨¬p O (IsSup A uzc ax ) + ... | case1 is-sup = ? -- x is a sup of zc + ... | case2 ¬x=sup = ? where -- x is not f y' nor sup of former ZChain from y -- no extention + chainf0 : (zc : ZChain1 A f mf ay x ) → (z : Ordinal) → z o< x → HOD + chainf0 zc z z<x with ZChain1.chain-uniq zc0 + ... | t = ? + supf : Ordinal → HOD + supf x = ZChain1.chain zc0 + Uz : HOD + Uz = UnionCF A x ( chainf0 zc0 ) + 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 - seq<x : {b : Ordinal } → (b<x : b o< x ) → ZChain1.chain zc0 ≡ supf0 b - seq<x {b} b<x with trio< b x - ... | tri< a ¬b ¬c = {!!} -- cong (λ k → (ZChain1.chain zc0) 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 - 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 + SZ0 : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → (x : Ordinal) → ZChain1 A f mf ay x ∧ ZChain A f mf ay x + SZ0 f mf ay x = TransFinite {λ z → ZChain1 A f mf ay z ∧ ZChain 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 (& A) (SZ0 f mf ay (& A)) - SZ f mf {y} ay = TransFinite {λ z → (zc1 : ZChain1 A f mf ay z ) → ZChain A f mf ay z zc1 } (λ x zc0 → ind f mf ay x zc0 ) (& A) (SZ0 f mf ay (& A)) + SZ : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → {y : Ordinal} (ay : odef A y) → ZChain A f mf ay (& A) + SZ f mf {y} ay = TransFinite {λ z → (zc1 : ZChain1 A f mf ay z ) → ZChain A f mf ay z } (λ x zc0 → ind f mf ay x zc0 ) (& A) ? zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) -- we have no Level (suc n) LEM @@ -723,8 +695,8 @@ 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) ) ⟫ 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 (& A) (zc0 (& A)) + zc0 x = proj1 ( 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 (& 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