Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 1219:91740267e62d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZProduct
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 06 Mar 2023 12:29:15 +0900
parents 362e43a1477c
children a8253c91f630
files src/Tychonoff.agda src/ZProduct.agda
diffstat 2 files changed, 28 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Mon Mar 06 10:45:34 2023 +0900
+++ b/src/Tychonoff.agda	Mon Mar 06 12:29:15 2023 +0900
@@ -446,7 +446,15 @@
                   ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋  ZFP q Q
                   ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq
              ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q)
-             ty02 = ?
+             ty02 {p} {q} record { z = zp ; az = azp ; x=ψz = x=ψzp } record { z = zq ; az = azq ; x=ψz = x=ψzq } Ppq 
+                = FPSet∋zpq (λ {z} xz → Ppq z (subst (λ k → odef k z) (sym *iso) xz )) ty50 where
+                  ty52 : filter F ∋ ZFP p Q 
+                  ty52 = ?
+                  ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
+                  ty51 = filter2 F ? ? ?
+                  ty50 : filter F ∋ ZFP (p ∩ q) Q
+                  ty50 = ?
+
 
          UFP : ultra-filter FP
          UFP = record { proper = {!!} ; ultra = {!!} }
--- a/src/ZProduct.agda	Mon Mar 06 10:45:34 2023 +0900
+++ b/src/ZProduct.agda	Mon Mar 06 12:29:15 2023 +0900
@@ -224,3 +224,22 @@
 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)
 
+ZFP∩  : {A B C : HOD} → ( ZFP (A ∩ B) C ≡ ZFP A C ∩ ZFP B C ) ∧ ( ZFP C (A ∩ B) ≡ ZFP C A  ∩ ZFP C B )
+proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00  ; eq← = zfp01 } where
+   zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x
+   zfp00  (ab-pair ⟪ pa , pb ⟫ qx) = ⟪ ab-pair pa qx  , ab-pair pb qx  ⟫
+   zfp01 : {x : Ordinal} → odef (ZFP A C ∩ ZFP B C) x → ZFProduct (A ∩ B) C x
+   zfp01 ⟪ p , q ⟫  = subst (λ k → ZFProduct (A ∩ B) C k) ? ( ab-pair (zfp02 ⟪ p , q ⟫ ) (zfp04 q) ) where
+       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 ? ⟫ where
+           zfp03 : {x : Ordinal } →  (bc : odef (ZFP B C) x) → x ≡ (& < * a , * b >)  → odef B (zπ1 (ab-pair {A} {C} ax bx))
+           zfp03 (ab-pair x x₁) eq = ?
+       zfp04 : {x : Ordinal } (acx : odef (ZFP B C) x )→ odef C (zπ2 acx)
+       zfp04 (ab-pair x x₁) = x₁
+proj2 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = ? ; eq← = ?  }
+
+
+
+
+
+