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

changeset 1232:2839815e7b50

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 18:47:07 +0900
parents d20199031218
children 61fc99e65055
files src/Tychonoff.agda
diffstat 1 files changed, 3 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Wed Mar 08 17:36:15 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 08 18:47:07 2023 +0900
@@ -505,9 +505,11 @@
              Rx = Replace' (* z) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy)))
              RxQ∋z : * z ⊆ ZFP Rx Q 
              RxQ∋z {w} zw = subst (λ k → ZFProduct Rx Q k ) ty70 ( ab-pair record { z = w ; az = zw ; x=ψz = refl  } (zp2 (f⊆L F az _ zw ) ) ) where
+                 a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) 
+                 b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw )
                  ty70 : & < * (& (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw))))) 
                       , * (zπ2 (f⊆L F az w zw)) > ≡ w
-                 ty70 = ?
+                 ty70 = trans (cong₂ (λ j k → & < * j , k > ) (trans &iso (cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b ))))  refl ) (trans ?  (zp-iso (f⊆L F az _ zw ) ))
              ty71 : * z ⊆ ZFP (* x) Q
              ty71 = subst (λ k → * z ⊆ ZFP k Q) ty72 RxQ∋z where
                  ty72 : Rx ≡ * x