# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678296701 -32400
# Node ID d2506e861dbf62c3e41daa6b5aae41a1035fd99a
# Parent  90e0e9fde1d63a3c0581994577d37c84a3f1c013
almost done

diff -r 90e0e9fde1d6 -r d2506e861dbf src/Tychonoff.agda
--- a/src/Tychonoff.agda	Wed Mar 08 21:26:40 2023 +0900
+++ b/src/Tychonoff.agda	Thu Mar 09 02:31:41 2023 +0900
@@ -35,7 +35,7 @@
 open import filter O
 open import ZProduct O
 open import Topology O
--- open import maximum-filter O
+open import maximum-filter O
 
 open Filter
 open Topology
@@ -152,11 +152,11 @@
      -- then we have maximum ultra filter
      --
      maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-     maxf {X} 0<X CSX fp = {!!} -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
      ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-     ultraf {X} 0<X CSX fp = {!!} -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      --
      -- so i has a limit as a limit of UIP
      --
@@ -504,21 +504,17 @@
              Rx : HOD
              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
+             RxQ∋z {w} zw = subst (λ k → ZFProduct Rx Q k ) ty70 ( ab-pair record { z = w ; az = zw ; x=ψz = refl  } (zp2 b )) 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 )
-                 ty71 : & (* (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)))) 
-                     ≡ zπ1 (subst (λ k → odef (ZFP P Q) k ) (sym &iso) ( f⊆L F az w zw ))  
-                 ty71 = begin
-                     & (* (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 > ) ty72 refl )  (zp-iso (f⊆L F az _ zw ) )
+                 ty73 : & (* (zπ1 a)) ≡ zπ1 b 
+                 ty73 = begin
+                     & (* (zπ1 a)) ≡⟨ &iso ⟩ 
+                     zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b)) ⟩ 
+                     zπ1 b ∎  where open ≡-Reasoning
+                 ty70 : & < * (& (* (zπ1 a))) , * (zπ2 b) > ≡ w
+                 ty70 with zp-iso (subst (λ k → odef (ZFP P Q) k) (sym &iso) (f⊆L F az _ zw )) 
+                 ... | eq = trans (cong₂ (λ j k → & < * j , k > ) ty73  refl ) (trans eq &iso ) 
              ty71 : * z ⊆ ZFP (* x) Q
              ty71 = subst (λ k → * z ⊆ ZFP k Q) ty72 RxQ∋z where
                  ty72 : Rx ≡ * x 
@@ -530,12 +526,17 @@
              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)) 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 ) 
+                 ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef P k) (sym ty84) ty87 where
+                      a =  f⊆L F (subst (odef (filter F)) (sym &iso) az) (& (* z1)) 
+                                 (subst (λ k → odef k (& (* z1))) (sym *iso) (subst (odef (* z)) (sym &iso) az1))
+                      b = subst (λ k → odef (ZFP P Q) k ) (sym &iso) (f⊆L F az _ az1 )
+                      ty87 : odef P (zπ1 b)
+                      ty87 = zp1 b
+                      ty84 : w ≡ (zπ1 b)
+                      ty84 = begin
+                       w ≡⟨ trans x=ψz1 &iso ⟩
+                       zπ1 a ≡⟨ cong zπ1 (HE.≅-to-≡ (∋-irr {ZFP _ _ } a b )) ⟩
+                       zπ1 b  ∎ where open ≡-Reasoning
 
          --  copy and pasted, sorry
          --
@@ -687,9 +688,6 @@
 
          Pf : odef (ZFP P Q) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >)
          Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq)
-         record aSubbase (b : Ordinal) : Set n where
-           field
-             fp∋b∨fq∋b : odef (filter FP ) b ∨ odef (filter FP ) b
 
          isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v
          isL {v} nei = filter1 F (λ z xz → Neighbor.v⊆P nei (subst (λ k → odef k z) *iso xz))