Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1477:88fdc41868f9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 29 Jun 2024 15:57:38 +0900 |
| parents | 32001d93755b |
| children | 623b2f792154 |
| files | src/OD.agda src/ZProduct.agda src/filter-util.agda src/maximum-filter.agda src/zorn.agda |
| diffstat | 5 files changed, 179 insertions(+), 147 deletions(-) [+] |
line wrap: on
line diff
--- a/src/OD.agda Fri Jun 28 20:55:38 2024 +0900 +++ b/src/OD.agda Sat Jun 29 15:57:38 2024 +0900 @@ -336,7 +336,7 @@ record RXCod (X COD : HOD) (ψ : (x : HOD) → X ∋ x → HOD) : Set (suc n) where field ≤COD : ∀ {x : HOD } → (lt : X ∋ x) → ψ x lt ⊆ COD - ψ-eq : ∀ {x : HOD } → (lt lt1 : X ∋ x) → ψ x lt ≡ ψ x lt1 + ψ-eq : ∀ {x : HOD } → (lt lt1 : X ∋ x) → ψ x lt =h= ψ x lt1 record Replaced1 (A : HOD) (ψ : (x : Ordinal ) → odef A x → Ordinal ) (x : Ordinal ) : Set n where field @@ -380,12 +380,12 @@ (λ z xz → & (ψ (* z) (eq→ *iso (subst (odef (* (& X))) (sym &iso) xz)))) x → Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x ri0 {x} record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = eq→ *iso az - ; x=ψz = trans x=ψz (cong (&) (RXCod.ψ-eq rc _ _ )) } + ; x=ψz = trans x=ψz (==→o≡ (RXCod.ψ-eq rc _ _ )) } ri1 : {x : Ordinal} → Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x → Replaced1 (* (& X)) (λ z xz → & (ψ (* z) (eq→ *iso (subst (odef (* (& X))) (sym &iso) xz)))) x ri1 {x} record { z = z ; az = az ; x=ψz = x=ψz } = record { z = z ; az = eq← *iso az - ; x=ψz = trans x=ψz (cong (&) (RXCod.ψ-eq rc _ _ )) } + ; x=ψz = trans x=ψz (==→o≡ (RXCod.ψ-eq rc _ _ )) } _∈_ : ( A B : HOD ) → Set n A ∈ B = B ∋ A
--- a/src/ZProduct.agda Fri Jun 28 20:55:38 2024 +0900 +++ b/src/ZProduct.agda Sat Jun 29 15:57:38 2024 +0900 @@ -190,6 +190,10 @@ proj1 (ZFP⊆ {A} {B} {a} a⊆A) (ab-pair x x₁) = ab-pair (a⊆A x) x₁ proj2 (ZFP⊆ {A} {B} {a} a⊆A) (ab-pair x x₁) = ab-pair x (a⊆A x₁) +ZFP-cong : {A B C D : HOD} → A =h= C → B =h= D → ZFP A B =h= ZFP C D +eq→ (ZFP-cong {A} {B} {C} {D} a=c b-d ) {w} (ab-pair x y) = ab-pair (eq→ a=c x) (eq→ b-d y) +eq← (ZFP-cong {A} {B} {C} {D} a=c b-d ) {w} (ab-pair x y) = ab-pair (eq← a=c x) (eq← b-d y) + ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b → ZFP A B ∋ < a , b > ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → odef (ZFP A B) k ) (==→o≡ (prod-cong-== *iso *iso ) ) (ab-pair aa bb) @@ -319,6 +323,10 @@ ZP-proj1⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc ... | ab-pair {a} {b} aa bb = ab-pair record { b = _ ; aa = aa ; bb = bb ; c∋ab = cc } bb +ZP-proj1-cong : {A B C : HOD} → {cab1 cab2 : C ⊆ ZFP A B} → ZP-proj1 A B C cab1 =h= ZP-proj1 A B C cab2 +eq→ (ZP-proj1-cong {A} {B} {C} {cab1} {cab2}) {w} record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } +eq← (ZP-proj1-cong {A} {B} {C} {cab1} {cab2}) {w} record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } + ZP-proj1=rev : {A B a m : HOD} {b : Ordinal } → {cab : m ⊆ ZFP A B} → odef B b → a ⊆ A → m =h= ZFP a B → a =h= ZP-proj1 A B m cab ZP-proj1=rev {A} {B} {a} {m} {b} {cab} bb a⊆A m=aB = record { eq→ = zp00 ; eq← = zp01 } where zp00 : {x : Ordinal} → odef a x → ZP1 A B m cab x @@ -329,12 +337,12 @@ zp02 {z} eq mab with eq→ m=aB mab ... | ab-pair {w1} {w2} aw1 bw2 = subst (λ k → odef a k ) (proj1 (prod-≡ eq )) aw1 -ZP-proj1-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj1 A B (* z) zab ≡ od∅ → z ≡ & od∅ +ZP-proj1-0 : {A B : HOD} {z : Ordinal } → {zab : * z ⊆ ZFP A B} → ZP-proj1 A B (* z) zab =h= od∅ → z ≡ & od∅ ZP-proj1-0 {A} {B} {z} {zab} eq = uf10 where uf10 : z ≡ & od∅ uf10 = trans (sym &iso) ( ¬x∋y→x≡od∅ (λ {y} zy → uf11 zy ) ) where uf11 : {y : Ordinal } → odef (* z) y → ⊥ - uf11 {y} zy = ⊥-elim ( ¬x<0 (subst (λ k → odef k (zπ1 pqy)) eq uf12 ) ) where + uf11 {y} zy = ⊥-elim ( ¬x<0 (eq→ eq uf12 ) ) where pqy : odef (ZFP A B) y pqy = zab zy uf14 : odef (* z) (& < * (zπ1 pqy) , * (zπ2 pqy) >) @@ -352,6 +360,10 @@ ZP-proj2 : (A B C : HOD) → C ⊆ ZFP A B → HOD ZP-proj2 A B C cab = record { od = record { def = λ x → ZP2 A B C cab x } ; odmax = & B ; <odmax = λ lt → odef< (ZP2.bb lt) } +ZP-proj2-cong : {A B C : HOD} → {cab1 cab2 : C ⊆ ZFP A B} → ZP-proj2 A B C cab1 =h= ZP-proj2 A B C cab2 +eq→ (ZP-proj2-cong {A} {B} {C} {cab1} {cab2}) {w} record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } +eq← (ZP-proj2-cong {A} {B} {C} {cab1} {cab2}) {w} record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } + ZP-proj2⊆ZFP : {A B C : HOD} → {cab : C ⊆ ZFP A B} → C ⊆ ZFP A (ZP-proj2 A B C cab) ZP-proj2⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc ... | ab-pair {a} {b} aa bb = ab-pair aa record { a = _ ; aa = aa ; bb = bb ; c∋ab = cc } @@ -388,8 +400,8 @@ fodmax = record { ≤COD = λ {x} ax → lemma1 ax ; ψ-eq = lemma2 } where lemma1 : {x : HOD} → (ax : odef A (& x)) → < x , * (func ax) > ⊆ Power (Union (A , B)) lemma1 {x} ax = ZFP<AB ax (subst (λ k → odef B k) (sym &iso) ( is-func ax ) ) - lemma2 : {x : HOD} (lt lt1 : A ∋ x) → < x , * (func lt) > ≡ < x , * (func lt1) > - lemma2 {x} lt1 lt2 = cong ( λ k → < x , * k > ) (func-wld lt1 lt2 refl ) + lemma2 : {x : HOD} (lt lt1 : A ∋ x) → < x , * (func lt) > =h= < x , * (func lt1) > + lemma2 {x} lt1 lt2 = prod-cong-== ==-refl (o≡→== (func-wld lt1 lt2 refl )) data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where
--- a/src/filter-util.agda Fri Jun 28 20:55:38 2024 +0900 +++ b/src/filter-util.agda Sat Jun 29 15:57:38 2024 +0900 @@ -49,10 +49,10 @@ filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → {x : HOD} → filter F ∋ x → { z : Ordinal } → odef x z → odef (ZFP P Q) z -filter-⊆ {P} {Q} F {x} fx {z} xz = f⊆L F fx _ (subst (λ k → odef k z) ? xz ) +filter-⊆ {P} {Q} F {x} fx {z} xz = f⊆L F fx _ (eq← *iso xz) rcp : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) P (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx)) -rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly } +rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly ; ψ-eq = λ {x} fx1 fx2 → ZP-proj1-cong } Filter-Proj1 : {P Q a : HOD } → ZFP P Q ∋ a → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) @@ -65,62 +65,58 @@ isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) fp00 : FP ⊆ Power P - fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) ? ) xw - ... | t = ? -- record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa + fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with eq→ *iso ( subst (λ k → odef (* k) w) x=ψz xw ) + ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa f0 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q f1 : {p q : HOD} → Power P ∋ q → FP ∋ p → p ⊆ q → FP ∋ q f1 {p} {q} Pq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP q Q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj1 } where PQq : Power (ZFP P Q) ∋ ZFP q Q - PQq z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans ? (cong (λ k → ZFP k Q) ?)) zpq ) + PQq z zpq = isP→PxQ {* (& q)} (Pq _) (eq→ (ZFP-cong (==-sym *iso) ==-refl) ( eq→ *iso zpq )) q⊆P : q ⊆ P - q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym ?) qw ) + q⊆P {w} qw = Pq _ (eq← *iso qw ) p⊆P : p ⊆ P p⊆P {w} pw = q⊆P (p⊆q pw) p=proj1 : & p ≡ & (ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az))) p=proj1 = x=ψz p⊆ZP : (* z) ⊆ ZFP p Q - p⊆ZP = subst (λ k → (* z) ⊆ ZFP k Q) (sym ?) ZP-proj1⊆ZFP + p⊆ZP lt = eq→ (ZFP-cong (==-sym ( ord→== p=proj1 )) ==-refl ) (ZP-proj1⊆ZFP lt) ty05 : filter F ∋ ZFP p Q - ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) ? wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP + ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (eq→ *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP ty06 : ZFP p Q ⊆ ZFP q Q ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq fp01 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq q=proj1 : & q ≡ & (ZP-proj1 P Q (* (& (ZFP q Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06)))) - q=proj1 = ? -- cong (&) (ZP-proj1=rev (zp2 pqa) q⊆P *iso ) + q=proj1 = ==→o≡ (ZP-proj1=rev (zp2 pqa) q⊆P *iso ) f2 : {p q : HOD} → FP ∋ p → FP ∋ q → Power P ∋ (p ∩ q) → FP ∋ (p ∩ q) f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq = record { z = _ ; az = ty50 ; x=ψz = pq=proj1 } where p⊆P : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ P - p⊆P {zp} {p} fzp p=proj1 {x} px with subst (λ k → odef k x) ? px - ... | t = ? -- record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa + p⊆P {zp} {p} fzp p=proj1 {x} px with eq→ (ord→== p=proj1) px + ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ & (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP p Q - x⊆pxq {zp} {p} fzp p=proj1 = subst (λ k → (* zp) ⊆ ZFP k Q) (sym ?) ZP-proj1⊆ZFP + x⊆pxq {zp} {p} fzp p=proj1 lt = eq→ (ZFP-cong (==-sym ( ord→== p=proj1 )) ==-refl ) (ZP-proj1⊆ZFP lt) ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q) ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where pqz : odef (ZFP (p ∩ q) Q) z - pqz = ? -- subst (λ k → odef k z ) (trans ? (sym (proj1 ZFP∩) )) xz + pqz = eq← (proj1 ZFP∩) (eq→ *iso xz) pqz1 : odef P (zπ1 pqz) pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz)) pqz2 : odef Q (zπ2 pqz) pqz2 = zp2 pqz ty53 : filter F ∋ ZFP p Q - ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp) - ?) - ? ? -- (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp) + ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp) (eq→ *iso wz )) (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp) ty52 : filter F ∋ ZFP q Q - ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq) - ?) - ? (x⊆pxq fzq x=ψzq) + ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq) (eq→ *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq) ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q ) ty51 = filter2 F ty53 ty52 ty54 ty50 : filter F ∋ ZFP (p ∩ q) Q - ty50 = subst (λ k → filter F ∋ k ) ? ty51 + ty50 = subst (λ k → odef (filter F) k ) (sym (==→o≡ (proj1 ZFP∩))) ty51 pq=proj1 : & (p ∩ q) ≡ & (ZP-proj1 P Q (* (& (ZFP (p ∩ q) Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50))) - pq=proj1 = ? -- cong (&) (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) ? pqx)) *iso ) + pq=proj1 = ==→o≡ (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (eq← *iso pqx)) *iso ) Filter-Proj1-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) @@ -129,29 +125,31 @@ FP = Filter-Proj1 pqa F ty60 : ¬ (filter FP ∋ od∅) ty60 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim (ultra-filter.proper UF - (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) ? x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where + (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (eq→ *iso x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where ty61 : * z ⊆ od∅ - ty61 {x} lt = ? -- ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj1-0 (sym ?))) *iso) lt )) + ty61 {x} lt = ⊥-elim (¬x<0 ty62 ) where + ty62 : odef od∅ x + ty62 = eq→ *iso (subst (λ k → odef (* k) x) (ZP-proj1-0 (ord→== (sym x=ψz)) ) lt ) ty62 : {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (filter (Filter-Proj1 pqa F) ∋ p) ∨ (filter (Filter-Proj1 pqa F) ∋ (P ＼ p)) ty62 {p} Pp NEGP = uf05 where p⊆P : p ⊆ P - p⊆P {z} px = Pp _ (subst (λ k → odef k z) ? px) + p⊆P {z} px = Pp _ (eq← *iso px) mp : HOD mp = ZFP p Q uf03 : Power (ZFP P Q) ∋ mp - uf03 x xz with subst (λ k → odef k x ) ? xz - ... | t = ? -- ab-pair ax by = ab-pair (p⊆P ax) by + uf03 x xz with eq→ *iso xz + ... | ab-pair ax by = ab-pair (p⊆P ax) by uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mp) - uf04 x xz = ? -- proj1 (subst (λ k → odef k x) *iso xz) + uf04 x xz = proj1 (eq→ *iso xz) uf02 : (filter F ∋ mp) ∨ (filter F ∋ (ZFP P Q ＼ mp)) uf02 = ultra-filter.ultra UF uf03 uf04 uf05 : (filter FP ∋ p) ∨ (filter FP ∋ (P ＼ p)) uf05 with uf02 - ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = ? } - ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = ? } + ... | case1 fp = case1 record { z = _ ; az = fp ; x=ψz = ==→o≡ (ZP-proj1=rev (zp2 pqa) p⊆P *iso ) } + ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = ==→o≡ (ZP-proj1=rev (zp2 pqa) proj1 (==-trans *iso (proj1 ZFP\Q))) } rcq : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) Q (λ x fx → ZP-proj2 P Q x (filter-⊆ F fx)) -rcq {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP2.bb ly } +rcq {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP2.bb ly ; ψ-eq = λ {x} fx1 fx2 → ZP-proj2-cong } -- -- Proj2 can be dervie from symmetry of ZFP (Product)
--- a/src/maximum-filter.agda Fri Jun 28 20:55:38 2024 +0900 +++ b/src/maximum-filter.agda Sat Jun 29 15:57:38 2024 +0900 @@ -1,47 +1,52 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} +open import Level +open import Ordinals +open import logic +open import Relation.Nullary open import Level open import Ordinals -module maximum-filter {n : Level } (O : Ordinals {n}) where +import HODBase +import OD +open import Relation.Nullary +module maximum-filter {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) + (AC : OD.AxiomOfChoice O HODAxiom ) where + + +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Data.Empty + +import OrdUtil + +open Ordinals.Ordinals O +open Ordinals.IsOrdinals isOrdinal +import ODUtil open import logic -import OD - -open import Relation.Nullary -open import Data.Empty -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality -import BAlgebra - -open BAlgebra O +open import nat -open inOrdinal O -open OD O -open OD.OD -open ODAxiom odAxiom - -import OrdUtil -import ODUtil -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal --- open Ordinals.IsNext isNext open OrdUtil O -open ODUtil O - - -import ODC -open ODC O +open ODUtil O HODAxiom ho< open _∧_ open _∨_ open Bool -open import filter O +open HODBase._==_ + +open HODBase.ODAxiom HODAxiom +open OD O HODAxiom + +open HODBase.HOD + +open AxiomOfChoice AC +open import ODC O HODAxiom AC as ODC + +open import filter O HODAxiom ho< AC +open import ZProduct O HODAxiom ho< open Filter - -open import Relation.Binary open import Relation.Binary.Structures PO : IsStrictPartialOrder _≡_ _⊂_
--- a/src/zorn.agda Fri Jun 28 20:55:38 2024 +0900 +++ b/src/zorn.agda Sat Jun 29 15:57:38 2024 +0900 @@ -1,11 +1,56 @@ -{-# OPTIONS --allow-unsolved-metas #-} -open import Level hiding ( suc ; zero ) +{-# OPTIONS --cubical-compatible --safe #-} +open import Level renaming (zero to Zero ; suc to Suc) open import Ordinals +open import logic +open import Relation.Nullary + +open import Ordinals +import HODBase +import OD +open import Relation.Nullary open import Relation.Binary -open import Relation.Binary.Core -open import Relation.Binary.PropositionalEquality -import OD -module zorn {n : Level } (O : Ordinals {n}) (_<_ : (x y : OD.HOD O ) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +module zorn {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O) (ho< : OD.ODAxiom-ho< O HODAxiom ) + (AC : OD.AxiomOfChoice O HODAxiom ) + (_<_ : (x y : OD.HOD O HODAxiom) → Set n ) (PO : IsStrictPartialOrder _≡_ _<_ ) where + + +-- open import Relation.Binary.Structures +open import Data.Empty +open import Data.Nat hiding ( _≤_ ; _<_ ) + +import OrdUtil + +open Ordinals.Ordinals O +open Ordinals.IsOrdinals isOrdinal +import ODUtil + +open import logic +open import nat + +open OrdUtil O +open ODUtil O HODAxiom ho< + +open _∧_ +open _∨_ +open Bool + +open HODBase._==_ + +open HODBase.ODAxiom HODAxiom +open OD O HODAxiom + +open HODBase.HOD + +open AxiomOfChoice AC +open import ODC O HODAxiom AC as ODC + +open import filter O HODAxiom ho< AC +open import ZProduct O HODAxiom ho< + +open Filter + -- -- Zorn-lemma : { A : HOD } @@ -14,35 +59,6 @@ -- → Maximal A -- -open import logic - -open import Relation.Nullary -open import Data.Empty -import BAlgebra - -open import Data.Nat hiding ( _<_ ; _≤_ ) -open import Data.Nat.Properties -open import nat - -open inOrdinal O -open OD O -open OD.OD -open ODAxiom odAxiom -import OrdUtil -import ODUtil -open Ordinals.Ordinals O -open Ordinals.IsOrdinals isOrdinal --- open Ordinals.IsNext isNext -open OrdUtil O -open ODUtil O - -import ODC - -open _∧_ -open _∨_ -open Bool - -open HOD -- -- Partial Order on HOD ( possibly limited in A ) @@ -85,7 +101,7 @@ ptrans = IsStrictPartialOrder.trans PO -open _==_ +-- open _==_ -- open _⊆_ -- we use different definition -- We cannot prove this without Well foundedness of A @@ -402,8 +418,8 @@ -- -- supf a over b and supf a is not included in UnionCF a nor UnionCF b, so UnionCF b is equal to the UnionCF a -- - union-max : {a b : Ordinal } → b o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b - union-max {a} {b} b≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where + union-max : {a b : Ordinal } → b o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a =h= UnionCF A f ay supf b + union-max {a} {b} b≤sa b≤z sa<sb = record { eq→ = z47 ; eq← = z48 } where z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w z47 {w} ⟪ aw , ch-init fc ⟫ = ⟪ aw , ch-init fc ⟫ z47 {w} ⟪ aw , ch-is-sup u u<a su=u fc ⟫ = ⟪ aw , ch-is-sup u u<b su=u fc ⟫ where @@ -422,7 +438,7 @@ x≤supfx→¬sa<sa : {a b : Ordinal } → b o≤ z → b o≤ supf a → ¬ (supf a o< supf b ) x≤supfx→¬sa<sa {a} {b} b≤z b≤sa sa<sb = ⊥-elim ( o<¬≡ z27 sa<sb ) where -- x o≤ supf a ∧ supf a o< supf b → ⊥, because it defines the same UnionCF z27 : supf a ≡ supf b - z27 = supfeq (ordtrans (supf-inject sa<sb) b≤z) b≤z ( union-max b≤sa b≤z sa<sb) + z27 = supfeq (ordtrans (supf-inject sa<sb) b≤z) b≤z ? -- ( union-max b≤sa b≤z sa<sb) order : {a b w : Ordinal } → b o≤ z → supf a o< supf b → FClosure A f (supf a) w → w ≤ supf b order {a} {b} {w} b≤z sa<sb fc = IsMinSUP.x≤sup (is-minsup b≤z) (cfcs (supf-inject sa<sb) b≤z sa<b fc) where @@ -448,7 +464,7 @@ f-total : IsTotalOrderSet chain f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-is-sup ub sub<x sub=ub fcb ⟫ = - subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso fc-total where + subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? fc-total where fc-total : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) fc-total with trio< ua ub ... | tri< a₁ ¬b ¬c with ≤-ftrans (order (o<→≤ sub<x) (subst₂ (λ j k → j o< k) (sym sua=ua) (sym sub=ub) a₁) fca ) (s≤fc (supf ub) f mf fcb ) @@ -466,24 +482,24 @@ ft01 : (& a) ≤ (& b) → Tri ( a < b) ( a ≡ b) ( b < a ) ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where a=b : a ≡ b - a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq) + a=b = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq) ft01 (case2 lt) = tri< a<b (λ eq → <-irr (case1 (sym eq)) a<b ) (λ lt → <-irr (case2 a<b ) lt) where a<b : a < b - a<b = subst₂ (λ j k → j < k ) *iso *iso lt + a<b = subst₂ (λ j k → j < k ) ? ? lt ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sub<x) fca) (s≤fc {A} _ f mf fcb)) f-total {a} {b} ⟪ uaa , ch-is-sup ua sua<x sua=ua fca ⟫ ⟪ uab , ch-init fcb ⟫ = ft00 where ft01 : (& b) ≤ (& a) → Tri ( a < b) ( a ≡ b) ( b < a ) ft01 (case1 eq) = tri≈ (λ lt → ⊥-elim (<-irr (case1 (sym a=b)) lt)) a=b (λ lt → ⊥-elim (<-irr (case1 a=b) lt)) where a=b : a ≡ b - a=b = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) (sym eq)) + a=b = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) (sym eq)) ft01 (case2 lt) = tri> (λ lt → <-irr (case2 b<a ) lt) (λ eq → <-irr (case1 eq) b<a ) b<a where b<a : b < a - b<a = subst₂ (λ j k → j < k ) *iso *iso lt + b<a = subst₂ (λ j k → j < k ) ? ? lt ft00 : Tri ( a < b) ( a ≡ b) ( b < a ) ft00 = ft01 (≤-ftrans (fcy<sup (o<→≤ sua<x) fcb) (s≤fc {A} _ f mf fca)) f-total {a} {b} ⟪ uaa , ch-init fca ⟫ ⟪ uab , ch-init fcb ⟫ = - subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp y f mf fca fcb ) + subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? (fcn-cmp y f mf fca fcb ) record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf< ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where @@ -505,7 +521,8 @@ supf-unique : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf< : <-monotonic-f A f) {y xa xb : Ordinal} → (ay : odef A y) → (xa o≤ xb ) → (za : ZChain A f mf< ay xa ) (zb : ZChain A f mf< ay xb ) → {z : Ordinal } → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z -supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa where +supf-unique A f mf< {y} {xa} {xb} ay xa≤xb za zb {z} z≤xa = ? where + -- Ordinals.inOrdinal.TransFinite0 {λ z → z o≤ xa → ZChain.supf za z ≡ ZChain.supf zb z } ind z z≤xa where supfa = ZChain.supf za supfb = ZChain.supf zb ind : (x : Ordinal) → ((w : Ordinal) → w o< x → w o≤ xa → supfa w ≡ supfb w) → x o≤ xa → supfa x ≡ supfb x @@ -560,13 +577,13 @@ z07 : {y : Ordinal} {A : HOD } → {P : Set n} → odef A y ∧ P → y o< & A z07 {y} {A} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) s : HOD - s = ODC.minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) + s = minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) as : A ∋ * ( & s ) - as = 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 )) ) + as = subst (λ k → odef A (& k) ) ? ( x∋minimal A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) as0 : odef A (& s ) as0 = subst (λ k → odef A k ) &iso as s<A : & s o< & A - s<A = c<→o< (subst (λ k → odef A (& k) ) *iso as ) + s<A = c<→o< (subst (λ k → odef A (& k) ) ? as ) 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) )) → ⊥ @@ -575,7 +592,7 @@ Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = z07 } z08 : ¬ Maximal A → HasMaximal =h= od∅ z08 nmx = record { eq→ = λ {x} lt → ⊥-elim ( nmx record {maximal = * x ; as = subst (λ k → odef A k) (sym &iso) (proj1 lt) - ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) *iso (proj2 lt (& y) ay) } ) ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )} + ; ¬maximal<x = λ {y} ay → subst (λ k → ¬ (* x < k)) ? (proj2 lt (& y) ay) } ) ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )} x-is-maximal : ¬ Maximal A → {x : Ordinal} → (ax : odef A x) → & (Gtx (subst (λ k → odef A k ) (sym &iso) ax)) ≡ o∅ → (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m)) x-is-maximal nmx {x} ax nogt m am = ⟪ subst (λ k → odef A k) &iso (subst (λ k → odef A k ) (sym &iso) ax) , ¬x<m ⟫ where ¬x<m : ¬ (* x < * m) @@ -590,15 +607,15 @@ xsup sup = {w : Ordinal } → odef B w → (w ≡ sup ) ∨ (w << sup ) ∀-imply-or : {A : Ordinal → Set n } {B : Set n } → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B - ∀-imply-or {A} {B} ∀AB with ODC.p∨¬p O ((x : Ordinal ) → A x) -- LEM + ∀-imply-or {A} {B} ∀AB with p∨¬p ((x : Ordinal ) → A x) -- LEM ∀-imply-or {A} {B} ∀AB | case1 t = case1 t ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x not )) where lemma : ¬ ((x : Ordinal ) → A x) → B - lemma not with ODC.p∨¬p O B + lemma not with p∨¬p B lemma not | case1 b = b lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) m00 : (x : Ordinal ) → ( ( z : Ordinal) → z o< x → ¬ (odef A z ∧ xsup z) ) ∨ MinSUP A B - m00 x = TransFinite0 ind x where + m00 x = ? where -- Ordinals.inOrdinal.TransFinite0 ? x where ind : (x : Ordinal) → ((z : Ordinal) → z o< x → ( ( w : Ordinal) → w o< z → ¬ (odef A w ∧ xsup w )) ∨ MinSUP A B) → ( ( w : Ordinal) → w o< x → ¬ (odef A w ∧ xsup w) ) ∨ MinSUP A B ind x prev = ∀-imply-or m01 where @@ -608,7 +625,7 @@ ... | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim ( ¬a lt ) ) ... | tri< a ¬b ¬c with prev z a ... | case2 mins = case2 mins - ... | case1 not with ODC.p∨¬p O (odef A z ∧ xsup z) + ... | case1 not with p∨¬p (odef A z ∧ xsup z) ... | case1 mins = case2 record { sup = z ; isMinSUP = record { as = proj1 mins ; x≤sup = proj2 mins ; minsup = m04 } } where m04 : {sup1 : Ordinal} → odef A sup1 → ({w : Ordinal} → odef B w → (w ≡ sup1) ∨ (w << sup1)) → z o≤ sup1 m04 {s} as lt with trio< z s @@ -630,18 +647,18 @@ -- Uncountable ascending chain by axiom of choice cf : ¬ Maximal A → Ordinal → Ordinal - cf nmx x with ODC.∋-p O A (* x) + cf nmx x with ∋-p A (* x) ... | no _ = o∅ ... | yes ax with is-o∅ (& ( Gtx ax )) ... | yes nogt = -- no larger element, so it is maximal ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ ) - ... | no not = & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))) + ... | no not = & (minimal (Gtx ax) (λ eq → not (=od∅→≡o∅ eq))) is-cf : (nmx : ¬ Maximal A ) → {x : Ordinal} → odef A x → odef A (cf nmx x) ∧ ( * x < * (cf nmx x) ) - is-cf nmx {x} ax with ODC.∋-p O A (* x) + is-cf nmx {x} ax with ∋-p A (* x) ... | no not = ⊥-elim ( not (subst (λ k → odef A k ) (sym &iso) ax )) ... | yes ax with is-o∅ (& ( Gtx ax )) ... | yes nogt = ⊥-elim (no-maximum (z08 nmx) x ⟪ subst (λ k → odef A k) &iso ax , x-is-maximal nmx (subst (λ k → odef A k ) &iso ax) nogt ⟫ ) - ... | no not = ODC.x∋minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)) + ... | no not = x∋minimal (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)) --- --- infintie ascention sequence of f @@ -681,7 +698,7 @@ b o< x → (ab : odef A b) → HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) b → * a < * b → odef (UnionCF A f ay supf x) b - is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P + is-max {a} {b} ua b<x ab P a<b with or-exclude P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x)) ... | case2 sb<sx = m10 where @@ -715,7 +732,7 @@ b o< x → (ab : odef A b) → HasPrev A (UnionCF A f ay supf x) f b ∨ IsSUP A (UnionCF A f ay supf b) b → * a < * b → odef (UnionCF A f ay supf x) b - is-max {a} {b} ua b<x ab P a<b with ODC.or-exclude O P + is-max {a} {b} ua b<x ab P a<b with or-exclude P is-max {a} {b} ua b<x ab P a<b | case1 has-prev = is-max-hp x {a} {b} ua ab has-prev a<b is-max {a} {b} ua b<x ab P a<b | case2 is-sup with IsSUP.x≤sup (proj2 is-sup) (ZChain.chain∋init zc ) ... | case1 b=y = ⟪ subst (λ k → odef A k ) b=y ay , ch-init (subst (λ k → FClosure A f y k ) b=y (init ay refl )) ⟫ @@ -748,7 +765,7 @@ utotal : ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) {y : Ordinal} (ay : odef A y) → IsTotalOrderSet (uchain f mf ay) - utotal f mf {y} ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso uz01 where + utotal f mf {y} ay {a} {b} ca cb = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? uz01 where uz01 : Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) uz01 = fcn-cmp y f mf ca cb @@ -821,18 +838,18 @@ ptotal {a0} {b0} (case1 a) (case2 b) with zc02 a b ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where eq1 : a0 ≡ b0 - eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) + eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq ) ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where lt1 : a0 < b0 - lt1 = subst₂ (λ j k → j < k ) *iso *iso lt + lt1 = subst₂ (λ j k → j < k ) ? ? lt ptotal {b0} {a0} (case2 b) (case1 a) with zc02 a b ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where eq1 : a0 ≡ b0 - eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) + eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq ) ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1 where lt1 : a0 < b0 - lt1 = subst₂ (λ j k → j < k ) *iso *iso lt - ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp (supf0 px) f mf (proj1 a) (proj1 b)) + lt1 = subst₂ (λ j k → j < k ) ? ? lt + ptotal (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? (fcn-cmp (supf0 px) f mf (proj1 a) (proj1 b)) pcha : pchainpx ⊆ A pcha (case1 lt) = proj1 lt @@ -1200,7 +1217,7 @@ ptotalU : IsTotalOrderSet pchainU ptotalU {a} {b} ia ib with trio< (IChain-i (proj2 ia)) (IChain-i (proj2 ib)) ... | tri< ia<ib ¬b ¬c = ZChain.f-total (pzc (pic<x (proj2 ib))) (IC⊆ (proj2 ia) (proj2 ib) ia<ib) (pchainU⊆chain ib) - ... | tri≈ ¬a ia=ib ¬c = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso ( pcmp (proj2 ia) (proj2 ib) ia=ib ) where + ... | tri≈ ¬a ia=ib ¬c = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? ( pcmp (proj2 ia) (proj2 ib) ia=ib ) where pcmp : (ia : IChain ay supfz (& a)) → (ib : IChain ay supfz (& b)) → IChain-i ia ≡ IChain-i ib → Tri (* (& a) < * (& b)) (* (& a) ≡ * (& b)) (* (& b) < * (& a) ) pcmp (ic-init fca) (ic-init fcb) eq = fcn-cmp _ f mf fca fcb @@ -1232,7 +1249,7 @@ fc12 = ftrans<-≤ lt (subst (λ k → k ≤ & a) (sym (zeq _ _ (o<→≤ <-osuc) o≤-refl )) (s≤fc _ f mf fca ) ) pcmp (ic-isup i i<x s<x fca) (ic-isup i i<y s<y fcb) refl = fcn-cmp _ f mf fca (subst (λ k → FClosure A f k (& b)) pc01 fcb ) where pc01 : supfz i<y ≡ supfz i<x - pc01 = cong supfz o<-irr + pc01 = ? -- cong supfz o<-irr ... | tri> ¬a ¬b ib<ia = ZChain.f-total (pzc (pic<x (proj2 ia))) (pchainU⊆chain ia) (IC⊆ (proj2 ib) (proj2 ia) ib<ia) @@ -1261,18 +1278,18 @@ ptotalS {a0} {b0} (case1 a) (case2 b) with zc02 a b ... | case1 eq = tri≈ (<-irr (case1 (sym eq1))) eq1 (<-irr (case1 eq1)) where eq1 : a0 ≡ b0 - eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) + eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq ) ... | case2 lt = tri< lt1 (λ eq → <-irr (case1 (sym eq)) lt1) (<-irr (case2 lt1)) where lt1 : a0 < b0 - lt1 = subst₂ (λ j k → j < k ) *iso *iso lt + lt1 = subst₂ (λ j k → j < k ) ? ? lt ptotalS {b0} {a0} (case2 b) (case1 a) with zc02 a b ... | case1 eq = tri≈ (<-irr (case1 eq1)) (sym eq1) (<-irr (case1 (sym eq1))) where eq1 : a0 ≡ b0 - eq1 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) eq ) + eq1 = subst₂ (λ j k → j ≡ k ) ? ? (cong (*) eq ) ... | case2 lt = tri> (<-irr (case2 lt1)) (λ eq → <-irr (case1 eq) lt1) lt1 where lt1 : a0 < b0 - lt1 = subst₂ (λ j k → j < k ) *iso *iso lt - ptotalS (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) *iso *iso (fcn-cmp spu0 f mf (proj1 a) (proj1 b)) + lt1 = subst₂ (λ j k → j < k ) ? ? lt + ptotalS (case2 a) (case2 b) = subst₂ (λ j k → Tri (j < k) (j ≡ k) (k < j)) ? ? (fcn-cmp spu0 f mf (proj1 a) (proj1 b)) S⊆A : pchainS ⊆ A S⊆A (case1 lt) = proj1 lt @@ -1302,7 +1319,7 @@ sf1=sf : {z : Ordinal } → (a : z o< x ) → supf1 z ≡ ZChain.supf (pzc (ob<x lim a)) z sf1=sf {z} z<x with trio< z x - ... | tri< a ¬b ¬c = cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr + ... | tri< a ¬b ¬c = ? -- cong ( λ k → ZChain.supf (pzc (ob<x lim k)) z) o<-irr ... | tri≈ ¬a b ¬c = ⊥-elim (¬a z<x) ... | tri> ¬a ¬b c = ⊥-elim (¬a z<x) @@ -1576,20 +1593,20 @@ zorn00 : Maximal A zorn00 with is-o∅ ( & HasMaximal ) - ... | no not = record { maximal = ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where + ... | no not = record { maximal = minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ; as = zorn01 ; ¬maximal<x = zorn02 } where -- yes we have the maximal because of the axiom of choice - zorn03 : odef HasMaximal ( & ( ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) - zorn03 = ODC.x∋minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) -- Axiom of choice - zorn01 : A ∋ ODC.minimal O HasMaximal (λ eq → not (=od∅→≡o∅ eq)) + zorn03 : odef HasMaximal ( & ( minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) ) ) + zorn03 = x∋minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) -- Axiom of choice + zorn01 : A ∋ minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) 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 ) + zorn02 : {x : HOD} → A ∋ x → ¬ (minimal HasMaximal (λ eq → not (=od∅→≡o∅ eq)) < x) + zorn02 {x} ax m<x = proj2 zorn03 (& x) ax (subst₂ (λ j k → j < k) ? ? m<x ) ... | yes ¬Maximal = ⊥-elim ( ¬Maximal→¬cf-mono nmx (SZ (cf nmx) (cf-is-<-monotonic nmx) as0 (& A) )) 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.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) *iso mx<y) ) ⟫ + zc5 = ⟪ Maximal.as mx , (λ y ay mx<y → Maximal.¬maximal<x mx (subst (λ k → odef A k ) (sym &iso) ay) (subst (λ k → k < * y) ? mx<y) ) ⟫ -- usage (see filter.agda ) --