Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1279:7e7d8d825632
P x Q ⇆ Q x P done
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 06 Apr 2023 09:16:52 +0900 |
| parents | 2cbe0db250da |
| children | a496dbb74a5f |
| files | src/Tychonoff.agda src/ZProduct.agda |
| diffstat | 2 files changed, 153 insertions(+), 126 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Tychonoff.agda Wed Apr 05 17:05:32 2023 +0900 +++ b/src/Tychonoff.agda Thu Apr 06 09:16:52 2023 +0900 @@ -35,7 +35,7 @@ open import filter O open import ZProduct O open import Topology O --- open import maximum-filter O +open import maximum-filter O open Filter open Topology @@ -80,6 +80,15 @@ P∋limit : odef P limit is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v) +-- +-- If Any ultra filter has a limit that is all neighbor of the limit is in the filter, +-- it has finite intersection property. +-- +-- Finite intersection defines a filter, so we have a ultra filter becaause Zorn lemma maximizing it. +-- If the limit of filter is not contained by a closed set p in FIP, it is in P \ p. It is open and +-- contains the limit, so it is in the ultra filter. This means p and P \ p is in the filter, which +-- contradicts proper of the ultra filter. +-- UFLP→FIP : {P : HOD} (TP : Topology P) → ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP UFLP→FIP {P} TP uflp with trio< (& P) o∅ @@ -176,13 +185,13 @@ -- otherwise the check requires a minute -- maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp) - maxf {X} 0<X CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) + maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x) mf {X} 0<X CSX fp = MaximumFilter.mf (maxf 0<X CSX fp) ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp) - ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) + ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp) -- - -- so it has a limit as a limit of UIP + -- so it has a limit as a limit of FIP -- limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal limit {X} CSX fp with trio< o∅ X @@ -243,6 +252,13 @@ P⊆Clx : {P : HOD} (TP : Topology P) → {x : HOD} → x ⊆ P → Cl TP x ⊆ P P⊆Clx {P} TP {x} x<p {y} xy = proj1 xy +-- +-- Finite intersection property implies that any ultra filter have a limit, that is, neighbors of the limit is in the filter. +-- +-- An ultra filter F is given. Take a closure of a filter. It is closed and it has finite intersection property, because F is porper. +-- So it has a limit as a FIP. If a neighbor p which contains the limit, p or P \ p is in the ultra filter. +-- If it is in P \ p, it cannot contains the limit, contradiction. +-- FIP→UFLP : {P : HOD} (TP : Topology P) → FIP TP → (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 @@ -345,18 +361,24 @@ postulate f-extensionality : { n m : Level} → Axiom.Extensionality.Propositional.Extensionality n m open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) - → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) -FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } +-- FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) +-- → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) +-- FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } +-- +-- projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) +-- → Filter {Power P} {P} (λ x → x) +-- projection-of-filter = ? +-- +-- projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) +-- → ultra-filter (projection-of-filter F) +-- projection-of-ultra-filter = ? -projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) - → Filter {Power P} {P} (λ x → x) -projection-of-filter = ? - -projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) - → ultra-filter (projection-of-filter F) -projection-of-ultra-filter = ? - +-- +-- We have UFLP both in P and Q. Given an ultra filter F on P x Q. It has limits on P and Q because a projection of ultra filter +-- is a ultra filter. Show the product of the limits is a limit of P x Q. A neighbor of P x Q contains subbase of P x Q, +-- which is either inverse projection x of P or Q. The x in in projection of F, because of UFLP. So it is in F, because of the +-- property of the filter. +-- Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q) → Compact TP → Compact TQ → Compact (ProductTopology TP TQ) Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where uflP : (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F)
--- a/src/ZProduct.agda Wed Apr 05 17:05:32 2023 +0900 +++ b/src/ZProduct.agda Thu Apr 06 09:16:52 2023 +0900 @@ -6,7 +6,7 @@ open import zf open import logic -import OD +import OD import ODUtil import OrdUtil @@ -16,7 +16,7 @@ open import Relation.Binary open import Relation.Binary.Core open import Relation.Binary.PropositionalEquality -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) open OD O open OD.OD @@ -40,10 +40,10 @@ exg-pair : { x y : HOD } → (x , y ) =h= ( y , x ) exg-pair {x} {y} = record { eq→ = left ; eq← = right } where - left : {z : Ordinal} → odef (x , y) z → odef (y , x) z + left : {z : Ordinal} → odef (x , y) z → odef (y , x) z left (case1 t) = case2 t left (case2 t) = case1 t - right : {z : Ordinal} → odef (y , x) z → odef (x , y) z + right : {z : Ordinal} → odef (y , x) z → odef (x , y) z right (case1 t) = case2 t right (case2 t) = case1 t @@ -57,12 +57,12 @@ eq-prod refl refl = refl xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y -xx=zy→x=y {x} {y} eq with trio< (& x) (& y) -xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) +xx=zy→x=y {x} {y} eq with trio< (& x) (& y) +xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a ) xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a ) xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b -xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl) +xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c with eq← eq {& y} (case2 refl) xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c ) xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c ) @@ -83,7 +83,7 @@ ... | refl = refl lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z lemmax : x ≡ x' - lemmax with eq→ eq {& (x , x)} (case1 refl) + lemmax with eq→ eq {& (x , x)} (case1 refl) lemmax | case1 s = lemma1 (ord→== s ) -- (x,x)≡(x',x') lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y' ... | refl = lemma1 (ord→== s ) @@ -118,14 +118,14 @@ ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) ) ZFP : (A B : HOD) → HOD -ZFP A B = record { od = record { def = λ x → ZFProduct A B x } - ; odmax = odmax ( A ⊗ B ) ; <odmax = λ {y} px → <odmax ( A ⊗ B ) (lemma0 px) } +ZFP A B = record { od = record { def = λ x → ZFProduct A B x } + ; odmax = odmax ( A ⊗ B ) ; <odmax = λ {y} px → <odmax ( A ⊗ B ) (lemma0 px) } where lemma0 : {A B : HOD} {x : Ordinal} → ZFProduct A B x → odef (A ⊗ B) x lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by) ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b → ZFP A B ∋ < a , b > -ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) +ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a @@ -148,7 +148,7 @@ zz11 = zp-iso pab zp-iso0 : { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (zπ1 p ≡ a) ∧ (zπ2 p ≡ b) -zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) )) +zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) )) , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) ) ⟫ ZFP⊆⊗ : {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x @@ -160,13 +160,13 @@ zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa )) zfp01 : odef (ZFP A B) (& x) zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox - ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) + ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) ZPI1 : (A B : HOD) → HOD -ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) +ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) ZPI2 : (A B : HOD) → HOD -ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) +ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) ZFProj1-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a ZFProj1-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) @@ -176,89 +176,6 @@ ZFProj2-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq)) ... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d) -record Func (A B : HOD) : Set n where - field - func : {x : Ordinal } → odef A x → Ordinal - is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax ) - -data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where - felm : (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > ))) - -FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B -FuncHOD→F {A} {B} (felm F) = F - -FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡ Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > ) -FuncHOD=R {A} {B} (felm F) = *iso - --- --- Set of All function from A to B --- - -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) - -Funcs : (A B : HOD) → HOD -Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B)) - ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where - lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x - lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx - ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k) - (sym x=ψz) lemma4 where - lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > ) - lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az)) - -record Injection (A B : Ordinal ) : Set n where - field - i→ : (x : Ordinal ) → odef (* A) x → Ordinal - iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt ) - iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y - -record HODBijection (A B : HOD ) : Set n where - field - fun← : (x : Ordinal ) → odef A x → Ordinal - fun→ : (x : Ordinal ) → odef B x → Ordinal - funB : (x : Ordinal ) → ( lt : odef A x ) → odef B ( fun← x lt ) - funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun→ x lt ) - fiso← : (x : Ordinal ) → ( lt : odef B x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x - fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x - -hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b -hodbij-refl {a} refl = record { - fun← = λ x _ → x - ; fun→ = λ x _ → x - ; funB = λ x lt → lt - ; funA = λ x lt → lt - ; fiso← = λ x lt → refl - ; fiso→ = λ x lt → refl - } - -pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) → - (zπ1 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ1 ab ))) ∧ - (zπ2 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ2 ab ))) -pj12 A B (ab-pair {x} {y} ax by) = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (prod-≡ pj24 ))) - , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (prod-≡ pj24))) ⟫ where - pj22 : odef (ZFP A B) (& (* (& < * x , * y >))) - pj22 = subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by) - pj23 : & < * (zπ1 pj22 ) , * (zπ2 pj22) > ≡ & (* (& < * x , * y >) ) - pj23 = zp-iso pj22 - pj24 : < * (zπ1 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) , * (zπ2 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) > - ≡ < * (& (* x)) , * (& (* y)) > - pj24 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( trans pj23 (trans &iso - (sym (cong (&) (cong₂ (λ j k → < j , k >) *iso *iso)) )))) -pj02 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab) -pj02 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj2 (pj12 A B ab))) (sym &iso)) } -pj01 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI1 A B) (zπ1 ab) -pj01 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj1 (pj12 A B ab))) (sym &iso)) } -pj2 : (A B : HOD) (x : Ordinal) (lt : odef (ZFP A B) x) → odef (ZFP (ZPI2 A B) (ZPI1 A B)) (& < * (zπ2 lt) , * (zπ1 lt) >) -pj2 A B x ab = ab-pair (pj02 A B x ab) (pj01 A B x ab) -aZPI1 : (A B : HOD) {y : Ordinal} → odef (ZPI1 A B) y → odef A y -aZPI1 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef A k) (trans ( - trans (sym &iso) (trans (sym (proj1 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp1 az ) -aZPI2 : (A B : HOD) {y : Ordinal} → odef (ZPI2 A B) y → odef B y -aZPI2 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef B k) (trans ( - trans (sym &iso) (trans (sym (proj2 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp2 az ) -pj1 : (A B : HOD) (x : Ordinal) (lt : odef (ZFP (ZPI2 A B) (ZPI1 A B)) x) → odef (ZFP A B) (& < * (zπ2 lt) , * (zπ1 lt) >) -pj1 A B _ (ab-pair ax by) = ab-pair (aZPI1 A B by) (aZPI2 A B ax) - ZPI1-iso : (A B : HOD) → {b : Ordinal } → odef B b → ZPI1 A B ≡ A ZPI1-iso P Q {q} qq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where ty21 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >))) @@ -311,6 +228,91 @@ * x ≡⟨ sym (cong (*) (ty32 pp qx )) ⟩ * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx ))) ∎ where open ≡-Reasoning +record Func (A B : HOD) : Set n where + field + func : {x : Ordinal } → odef A x → Ordinal + is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax ) + +data FuncHOD (A B : HOD) : (x : Ordinal) → Set n where + felm : (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > ))) + +FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B +FuncHOD→F {A} {B} (felm F) = F + +FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡ Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > ) +FuncHOD=R {A} {B} (felm F) = *iso + +-- +-- Set of All function from A to B +-- + +open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) + +Funcs : (A B : HOD) → HOD +Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B)) + ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where + lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x + lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx + ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k) + (sym x=ψz) lemma4 where + lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > ) + lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az)) + +record Injection (A B : Ordinal ) : Set n where + field + i→ : (x : Ordinal ) → odef (* A) x → Ordinal + iB : (x : Ordinal ) → ( lt : odef (* A) x ) → odef (* B) ( i→ x lt ) + iiso : (x y : Ordinal ) → ( ltx : odef (* A) x ) ( lty : odef (* A) y ) → i→ x ltx ≡ i→ y lty → x ≡ y + +record HODBijection (A B : HOD ) : Set n where + field + fun← : (x : Ordinal ) → odef A x → Ordinal + fun→ : (x : Ordinal ) → odef B x → Ordinal + funB : (x : Ordinal ) → ( lt : odef A x ) → odef B ( fun← x lt ) + funA : (x : Ordinal ) → ( lt : odef B x ) → odef A ( fun→ x lt ) + fiso← : (x : Ordinal ) → ( lt : odef B x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x + fiso→ : (x : Ordinal ) → ( lt : odef A x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x + +hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b +hodbij-refl {a} refl = record { + fun← = λ x _ → x + ; fun→ = λ x _ → x + ; funB = λ x lt → lt + ; funA = λ x lt → lt + ; fiso← = λ x lt → refl + ; fiso→ = λ x lt → refl + } + +pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) → + (zπ1 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ1 ab ))) ∧ + (zπ2 (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ2 ab ))) +pj12 A B (ab-pair {x} {y} ax by) = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (prod-≡ pj24 ))) + , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (prod-≡ pj24))) ⟫ where + pj22 : odef (ZFP A B) (& (* (& < * x , * y >))) + pj22 = subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by) + pj23 : & < * (zπ1 pj22 ) , * (zπ2 pj22) > ≡ & (* (& < * x , * y >) ) + pj23 = zp-iso pj22 + pj24 : < * (zπ1 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) , * (zπ2 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) > + ≡ < * (& (* x)) , * (& (* y)) > + pj24 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( trans pj23 (trans &iso + (sym (cong (&) (cong₂ (λ j k → < j , k >) *iso *iso)) )))) +pj02 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab) +pj02 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj2 (pj12 A B ab))) (sym &iso)) } +pj01 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI1 A B) (zπ1 ab) +pj01 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj1 (pj12 A B ab))) (sym &iso)) } + +pj2 : (A B : HOD) (x : Ordinal) (lt : odef (ZFP A B) x) → odef (ZFP (ZPI2 A B) (ZPI1 A B)) (& < * (zπ2 lt) , * (zπ1 lt) >) +pj2 A B x ab = ab-pair (pj02 A B x ab) (pj01 A B x ab) + +aZPI1 : (A B : HOD) {y : Ordinal} → odef (ZPI1 A B) y → odef A y +aZPI1 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef A k) (trans ( + trans (sym &iso) (trans (sym (proj1 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp1 az ) +aZPI2 : (A B : HOD) {y : Ordinal} → odef (ZPI2 A B) y → odef B y +aZPI2 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef B k) (trans ( + trans (sym &iso) (trans (sym (proj2 (pj12 A B az))) (sym &iso))) (sym x=ψz) ) ( zp2 az ) + +pj1 : (A B : HOD) (x : Ordinal) (lt : odef (ZFP (ZPI2 A B) (ZPI1 A B)) x) → odef (ZFP A B) (& < * (zπ2 lt) , * (zπ1 lt) >) +pj1 A B _ (ab-pair ax by) = ab-pair (aZPI1 A B by) (aZPI2 A B ax) ZFPsym1 : (A B : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B)) ZFPsym1 A B = record { @@ -321,13 +323,16 @@ ; fiso← = λ xy ab → pj00 A B ab ; fiso→ = λ xy ab → zp-iso ab } where - pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) + pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) → & < * (zπ1 ab) , * (zπ2 ab) > ≡ & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > pj10 A B {.(& < * _ , * _ >)} (ab-pair ax by ) = refl - pj00 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) - → & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > ≡ xy + pj00 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) + → & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > ≡ xy pj00 A B {xy} ab = trans (sym (pj10 A B ab)) (zp-iso {ZPI2 A B} {ZPI1 A B} {xy} ab) +-- +-- Bijection of (A x B) and (B x A) requires one element or axiom of choice +-- ZFPsym : (A B : HOD) → {a b : Ordinal } → odef A a → odef B b → HODBijection (ZFP A B) (ZFP B A) ZFPsym A B aa bb = subst₂ ( λ j k → HODBijection (ZFP A B) (ZFP j k)) (ZPI2-iso A B aa) (ZPI1-iso A B bb) ( ZFPsym1 A B ) @@ -342,7 +347,7 @@ zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x zfp06 = zp-iso q zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x - zfp07 = trans (cong (λ k → & < k , * (zπ2 q) > ) + zfp07 = trans (cong (λ k → & < k , * (zπ2 q) > ) (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06)))))))) zfp06 zfp02 : {x : Ordinal } → (acx : odef (ZFP A C ∩ ZFP B C) x) → odef (A ∩ B) (zπ1 (proj1 acx)) zfp02 {.(& < * _ , * _ >)} ⟪ ab-pair {a} {b} ax bx , bcx ⟫ = ⟪ ax , zfp03 bcx refl ⟫ where @@ -351,7 +356,7 @@ zfp08 : a1 ≡ a zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj1 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq))))) zfp04 : {x : Ordinal } (acx : odef (ZFP B C) x )→ odef C (zπ2 acx) - zfp04 (ab-pair x x₁) = x₁ + zfp04 (ab-pair x x₁) = x₁ proj2 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01 } where zfp00 : {x : Ordinal} → ZFProduct C (A ∩ B) x → odef (ZFP C A ∩ ZFP C B) x zfp00 (ab-pair qx ⟪ pa , pb ⟫ ) = ⟪ ab-pair qx pa , ab-pair qx pb ⟫ @@ -362,7 +367,7 @@ zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x zfp06 = zp-iso q zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x - zfp07 = trans (cong (λ k → & < * (zπ1 p) , k > ) + zfp07 = trans (cong (λ k → & < * (zπ1 p) , k > ) (sym (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) (trans zfp05 (sym (zfp06))))))))) zfp05 zfp02 : {x : Ordinal } → (acx : odef (ZFP C A ∩ ZFP C B ) x) → odef (A ∩ B) (zπ2 (proj2 acx)) zfp02 {.(& < * _ , * _ >)} ⟪ bcx , ab-pair {b} {a} ax bx ⟫ = ⟪ zfp03 bcx refl , bx ⟫ where @@ -371,7 +376,7 @@ zfp08 : a1 ≡ a zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj2 (prod-≡ (subst₂ _≡_ *iso *iso (cong (*) eq))))) zfp04 : {x : Ordinal } (acx : odef (ZFP C A ) x )→ odef C (zπ1 acx) - zfp04 (ab-pair x x₁) = x + zfp04 (ab-pair x x₁) = x open import BAlgebra O @@ -381,16 +386,16 @@ ty70 ⟪ ab-pair {a} {b} Pa pb , npq ⟫ = ab-pair ty72 pb where ty72 : odef (P ＼ p ) a ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫ - ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x - ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb - , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ + ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x + ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb + , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ ty73 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP P p ) x → odef (ZFP P (Q ＼ p) ) x ty73 ⟪ ab-pair {a} {b} pa Qb , npq ⟫ = ab-pair pa ty72 where ty72 : odef (Q ＼ p ) b ty72 = ⟪ Qb , (λ qb → npq (ab-pair pa qb ) ) ⟫ - ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x - ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb - , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫ + ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x + ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb + , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫