Mercurial > hg > Members > kono > Proof > ZF-in-agda
view src/Tychonoff1.agda @ 1296:428227847d62
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 02 Jun 2023 12:12:29 +0900 |
parents | |
children | ad9ed7c4a0b3 |
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-Proj1 : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → Filter {Power P} {P} (λ x → x) Filter-Proj1 = ? 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 = ? 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 ) 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 a : HOD } → ZFP P Q ∋ a → (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} {z} pqz F = record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = ? } 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 = ? } where 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 ) ? fz where fig07 : Replaced1.z fqp ≡ & (ZPmirror Q P p (λ px → QPq x (subst (λ k → def (HOD.od k) x) (sym *iso) (p⊆q px)))) fig07 = ? fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP fig01 x xz = ? -- fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q fis00 = filter1 F fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP fis04 = ? fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04)))) fis05 = ? 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 pqa F )