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

changeset 1230:faffe9a4bd0f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 08 Mar 2023 15:36:35 +0900
parents 5e6dfe739f6a
children d20199031218
files src/Tychonoff.agda
diffstat 1 files changed, 13 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Wed Mar 08 14:10:56 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 08 15:36:35 2023 +0900
@@ -500,7 +500,19 @@
 
          --  FPSet is in Projection ⁻¹  F
          FPSet⊆F : {x : Ordinal } → odef FPSet x →  odef (filter F) (& (ZFP (* x) Q))
-         FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = ?
+         FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (filter F) k ) ty70 az where
+            ty70 : z ≡ & (ZFP (* x) Q)
+            ty70 = subst₂ ( λ j k → j ≡ k ) &iso refl (cong (&) (==→o≡ record { eq→  = ty71 ; eq← = ty74 } ) ) where
+               ty71 : {y : Ordinal } → odef (* z) y → odef (ZFP (* x) Q) y 
+               ty71 {y} zy = subst (λ k → ZFProduct (* x) Q k ) ty72 ( ab-pair ty73 aq ) where
+                  ty72 :  & < * ? , * (zπ2 is-apq) > ≡ y
+                  ty72 = ?
+                  ty73 : odef (* x) ?
+                  ty73 = subst (λ k → odef k ?) (trans (sym *iso) (sym (cong (*) x=ψz))) record {z = ? ; az = ? ; x=ψz = ? } 
+               ty74 : {y : Ordinal } → odef (ZFP (* x) Q) y  → odef (* z) y
+               ty74 {.(& < * _ , * _ >)} (ab-pair {a} {b} xx qy) with subst (λ k → odef k a) (sym (trans (sym *iso) (sym (cong (*) x=ψz)))) xx
+               ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = ?
+
 
          --  copy and pasted, sorry
          --