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

changeset 1234:90e0e9fde1d6

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 21:26:40 +0900
parents 61fc99e65055
children d2506e861dbf
files src/Tychonoff.agda
diffstat 1 files changed, 10 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/src/Tychonoff.agda	Wed Mar 08 19:52:41 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 08 21:26:40 2023 +0900
@@ -513,9 +513,12 @@
                      & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) ≡⟨ &iso ⟩ 
                      zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)) ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ 
                      zπ1 (subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ))  ∎ where open ≡-Reasoning
+                 ty72 : & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) 
+                     ≡ zπ1 (f⊆L F az w zw) 
+                 ty72 = ?
                  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 = trans (cong₂ (λ j k → & < * j , k > ) ? refl )  (zp-iso (f⊆L F az _ zw ) )
+                 ty70 = trans (cong₂ (λ j k → & < * j , k > ) ty72 refl )  (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 
@@ -527,8 +530,12 @@
              ty80 y yx = isP→PxQ ty81 (subst (λ k → odef k y ) *iso yx ) where
                  ty81 : * x ⊆ P 
                  ty81 {w} xw with subst (λ k → odef k w) (trans (cong (*) x=ψz ) *iso ) xw
-                 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (trans (sym &iso) (sym x=ψz1)) ?
-                     -- ( zp1 (f⊆L F az _ ? ) )
+                 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (trans (sym &iso) (sym x=ψz1)) ty82 where
+                      ty82 : odef P (zπ1 (f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) 
+                                 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1))))
+                      ty82 = ?
+                      ty83 : odef P (zπ1 (f⊆L F az z1 az1))
+                      ty83 = zp1 (f⊆L F az _ az1 ) 
 
          --  copy and pasted, sorry
          --