# HG changeset patch # User Shinji KONO # Date 1656888090 -32400 # Node ID 1002866230b8d4a450d83d34b2a9a2db11ac7a34 # Parent 6a8d13b02a508e5d38259077062931f63088e5c9 new TransFinite induction diff -r 6a8d13b02a50 -r 1002866230b8 src/zorn.agda --- a/src/zorn.agda Sun Jul 03 18:59:49 2022 +0900 +++ b/src/zorn.agda Mon Jul 04 07:41:30 2022 +0900 @@ -289,7 +289,7 @@ 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) (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) ( z : Ordinal ) (zc0 : ZChain1 A f mf ay z ) : Set (Level.suc n) where chain : HOD chain = ZChain1.chain zc0 field @@ -365,7 +365,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 : ZChain1 A f mf as0 (& A) ) (zc : ZChain A f mf as0 (& A) zc0 ) (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 +374,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 : ZChain1 A f mf as0 (& A)) (zc : ZChain A f mf as0 (& A) zc0 ) → (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 +423,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 : ZChain1 A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A)) (zc : ZChain A (cf nmx) (cf-is-≤-monotonic nmx) as0 (& A) zc0 ) → 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) ) @@ -477,16 +477,16 @@ chainq z z ¬a ¬b c = ⊥-elim (¬a b