Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/Tychonoff1.agda @ 1297:ad9ed7c4a0b3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 03 Jun 2023 08:13:50 +0900 |
| parents | 428227847d62 |
| children |
line wrap: on
line source
{-# OPTIONS --allow-unsolved-metas #-} open import Level open import Ordinals module Tychonoff1 {n : Level } (O : Ordinals {n}) where open import logic open _∧_ open _∨_ open Bool import OD open import Relation.Nullary open import Data.Empty open import Relation.Binary.Core open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality import BAlgebra open BAlgebra O 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 import filter O open import ZProduct O -- open import maximum-filter O open Filter 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) (sym *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 } Filter-Proj1 : {P Q a : HOD } → ZFP P Q ∋ a → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → Filter {Power P} {P} (λ x → x) Filter-Proj1 {P} {Q} pqa F = record { filter = FP ; f⊆L = fp00 ; filter1 = f1 ; filter2 = f2 } where FP : HOD FP = Replace' (filter F) (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx)) {P} (rcp F) isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q 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) *iso ) 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 *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq ) q⊆P : q ⊆ P q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *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 (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP ty05 : filter F ∋ ZFP p Q ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *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 ) 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) (&≡&→≡ 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 (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP 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 *iso (sym (proj1 ZFP∩) )) 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 k z) *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) (subst (λ k → odef k z) *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 ) (sym (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) (sym *iso) pqx)) *iso ) Filter-Proj1-UF : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) → (FP : Filter {Power P} {P} (λ x → x) ) → ultra-filter FP Filter-Proj1-UF = ? rcf : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly } Filter-sym : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) Filter-sym {P} {Q} F = record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = f2 } where fqp : HOD fqp = Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf F) fqp<P : fqp ⊆ Power (ZFP Q P) fqp<P {z} record { z = x ; az = fx ; x=ψz = x=ψz } w xw = ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) (subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw) f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 ; x=ψz = fis05 } where fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q fis00 = filter1 F q⊆ZQP : q ⊆ ZFP Q P q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) (sym *iso) qx) p⊆ZQP : p ⊆ ZFP Q P p⊆ZQP {z} px = q⊆ZQP (p⊆q px) fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fqp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fqp)))) fig06 = Replaced1.x=ψz fqp fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP fig03 with Replaced1.az fqp ... | fz = subst (λ k → odef (filter F) k ) fig07 fz where fig07 : Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (subst (λ k → def (HOD.od k) x ) (sym *iso) (p⊆q px)))) fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) ))))) fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (subst (λ k → odef k x) *iso xz) fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP fis04 = ZPmirror-⊆ p⊆q fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04)))) fis05 = cong (&) (sym ( ZPmirror-rev (sym *iso) )) f2 : {p q : HOD} → fqp ∋ p → fqp ∋ q → Power (ZFP Q P) ∋ (p ∩ q) → fqp ∋ (p ∩ q) f2 {p} {q} fp fq QPpq = record { z = _ ; az = fis12 {ZPmirror Q P p p⊆ZQP} {ZPmirror Q P q q⊆ZQP} fig03 fig04 fig01 ; x=ψz = fis05 } where fis12 : {p q : HOD} → filter F ∋ p → filter F ∋ q → Power (ZFP P Q) ∋ (p ∩ q) → filter F ∋ (p ∩ q) fis12 {p} {q} fp fq PQpq = filter2 F fp fq PQpq p⊆ZQP : p ⊆ ZFP Q P p⊆ZQP {z} px = fqp<P fp _ (subst (λ k → odef k z) (sym *iso) px) q⊆ZQP : q ⊆ ZFP Q P q⊆ZQP {z} qx = fqp<P fq _ (subst (λ k → odef k z) (sym *iso) qx) pq⊆ZQP : (p ∩ q) ⊆ ZFP Q P pq⊆ZQP {z} pqx = QPpq _ (subst (λ k → odef k z) (sym *iso) pqx) fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fp)))) fig06 = Replaced1.x=ψz fp fig09 : & q ≡ & (ZPmirror P Q (* (Replaced1.z fq)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fq)))) fig09 = Replaced1.x=ψz fq fig03 : filter F ∋ ZPmirror Q P p p⊆ZQP fig03 = subst (λ k → odef (filter F) k ) fig07 ( Replaced1.az fp ) where fig07 : Replaced1.z fp ≡ & (ZPmirror Q P p p⊆ZQP ) fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) ))))) fig04 : filter F ∋ ZPmirror Q P q q⊆ZQP fig04 = subst (λ k → odef (filter F) k ) fig08 ( Replaced1.az fq ) where fig08 : Replaced1.z fq ≡ & (ZPmirror Q P q q⊆ZQP ) fig08 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig09) ))))) fig01 : Power (ZFP P Q) ∋ ( ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP ) fig01 x xz = ZPmirror⊆ZFPBA Q P q q⊆ZQP (proj2 (subst (λ k → odef k x) *iso xz)) fis05 : & (p ∩ q) ≡ & (ZPmirror P Q (* (& (ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis12 fig03 fig04 fig01) ))) fis05 = cong (&) (sym ( ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} (trans ZPmirror-∩ (sym *iso) ) )) Filter-sym-UF : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) (UF : ultra-filter F) → (FQP : Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) ) → ultra-filter FQP Filter-sym-UF = ? Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → Filter {Power Q} {Q} (λ x → x) Filter-Proj2 {P} {Q} {a} pqa F = Filter-Proj1 {Q} {P} ? (Filter-sym F )