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

changeset 1220:a8253c91f630

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZFP distr
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 06 Mar 2023 15:23:17 +0900
parents 91740267e62d
children 0e8306b146f6
files src/Tychonoff.agda src/ZProduct.agda
diffstat 2 files changed, 48 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Mon Mar 06 12:29:15 2023 +0900
+++ b/src/Tychonoff.agda	Mon Mar 06 15:23:17 2023 +0900
@@ -448,12 +448,24 @@
              ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q)
              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 
+                  x⊆pxq : * ? ⊆ ZFP p Q
+                  x⊆pxq = ?
+                  ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q)
+                  ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso ty55) (ab-pair ty551 ty552 ) where
+                     ty55 :  odef (ZFP (p ∩ q) Q)  z
+                     ty55 = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) ))  xz
+                     ty551 :  odef P (zπ1 ty55)
+                     ty551 = ?
+                     ty552 :  odef Q (zπ2 ty55)
+                     ty552 = ?
+                  ty53 : filter F ∋ ZFP p Q 
+                  ty53 = filter1 F (λ z wz → isP→PxQ ? (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) ? ) x⊆pxq
+                  ty52 : filter F ∋ ZFP q Q 
                   ty52 = ?
                   ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
-                  ty51 = filter2 F ? ? ?
+                  ty51 = filter2 F ty53 ty52 ty54
                   ty50 : filter F ∋ ZFP (p ∩ q) Q
-                  ty50 = ?
+                  ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51
 
 
          UFP : ultra-filter FP
--- a/src/ZProduct.agda	Mon Mar 06 12:29:15 2023 +0900
+++ b/src/ZProduct.agda	Mon Mar 06 15:23:17 2023 +0900
@@ -229,14 +229,42 @@
    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
+   zfp01 {x} ⟪ p , q ⟫  = subst (λ k → ZFProduct (A ∩ B) C k) zfp07 ( ab-pair (zfp02 ⟪ p , q ⟫ ) (zfp04 q) ) where
+       zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x
+       zfp05 = zp-iso p
+       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)  >  ) 
+           (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 ? ⟫ where
+       zfp02 {.(& < * _ , * _ >)} ⟪ ab-pair {a} {b} ax bx , bcx ⟫ = ⟪ ax , zfp03 bcx refl ⟫ 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 = ?
+           zfp03 (ab-pair {a1} {b1} x x₁) eq = subst (λ k → odef B k ) zfp08 x  where
+              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₁
-proj2 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = ? ; eq← = ?  }
+       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   ⟫
+   zfp01 : {x : Ordinal} → odef (ZFP C A ∩ ZFP C B ) x → ZFProduct C (A ∩ B)  x
+   zfp01 {x} ⟪ p , q ⟫  = subst (λ k → ZFProduct C (A ∩ B)  k) zfp07 ( ab-pair (zfp04 p) (zfp02 ⟪ p , q ⟫ )  ) where
+       zfp05 : & < * (zπ1 p) , * (zπ2 p) > ≡ x
+       zfp05 = zp-iso p
+       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  >  ) 
+           (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
+           zfp03 : {x : Ordinal } →  (bc : odef (ZFP C A ) x) → x ≡ (& < * b , * a >)  → odef A (zπ2 (ab-pair {C} {B} ax bx ))
+           zfp03 (ab-pair {b1} {a1} x x₁) eq = subst (λ k → odef A k ) zfp08 x₁ where
+              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