# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719842657 -32400
# Node ID 0dbbae768c9024e1f498cff7f4193a613f75d130
# Parent  33116eb3abd148305783cef840db797e6bc655f6
...

diff -r 33116eb3abd1 -r 0dbbae768c90 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Mon Jul 01 18:15:45 2024 +0900
+++ b/src/Tychonoff.agda	Mon Jul 01 23:04:17 2024 +0900
@@ -201,21 +201,21 @@
               xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
               sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
               sbpq = sb⊆ {Np+Nq} {* (& Np+Nq)} (eq← *iso) (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
-              -- subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
               f20 : * (& Np+Nq) ⊆ * X
               f20 {x} npq with eq→ *iso npq
               ... | case1 np = FBase.b⊆X Np np
               ... | case2 nq = FBase.b⊆X Nq nq
               f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
-              f22 = ? -- subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
-                 -- → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
+              f22 {x} xxpq = eq←  *iso ⟪  eq→ *iso ( FBase.x⊆u Np (proj1 xpq)) , eq→ *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ where
+                    xpq :  odef (* (FBase.x Np) ∩ * (FBase.x Nq)) x
+                    xpq =  eq→ *iso xxpq
      --
      -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x )
      --
      proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅)
      proper {X} CSX fip record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = u⊆P ; x⊆u = x⊆u } = o≤> x≤0 (fip (fp00 _ _ b⊆X sb)) where
           x≤0 : x o< osuc  o∅
-          x≤0 = ? -- subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u))
+          x≤0 = subst₂ (λ j k → j o< osuc k) &iso (trans (==→o≡ {* (& od∅)} {* o∅} (==-trans *iso (==-sym o∅==od∅)  )) &iso) (⊆→o≤ (x⊆u))
           fp00 : (b x : Ordinal) → * b ⊆ * X → Subbase (* b) x → Subbase (* X) x
           fp00 b y b<X (gi by ) = gi ( b<X by )
           fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz)
@@ -273,8 +273,8 @@
         uf10 = nlxy
         uf03 : Neighbor TP y (& (P ＼ * x ))
         uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx))
-           ; ux = ? -- subst (λ k → odef k y) (sym *iso) uf10
-           ; v⊆P = ? -- λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz )
+           ; ux = eq← *iso uf10
+           ; v⊆P = λ {z} xz → proj1 (eq→ *iso xz )
            ; u⊆v = λ x → x  }
         uf07 : * (& (* x , * x)) ⊆ * X
         uf07 {y} lt with eq→ *iso lt
@@ -282,7 +282,7 @@
         ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx
         uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x
         uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07
-           ; sb = ? --- gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) )  
+           ; sb = gi (eq← *iso (case1 (sym &iso)) )  
            ; u⊆P = x⊆P ; x⊆u = λ x → x  }
         -- if we postulate maximum filter, uf061 is an error
         -- uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P ＼ * x ))))
@@ -293,7 +293,7 @@
         uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x ))
         uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso uf063
         uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅
-        uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ? ) where -- ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) }  ) ) where
+        uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) }  ) where
            uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y
            uf14 {y} ⟪ xy , ⟪ Px , ¬xy ⟫ ⟫ = ⊥-elim ( ¬xy xy )
         uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x )))
@@ -333,8 +333,11 @@
      --
      -- take closure of given filter elements
      --
+     Cl-cong : {x y : HOD} → od x == od y → Cl TP x =h= Cl TP y
+     eq→ (Cl-cong {x} {y} x=y) ⟪ Pz , cl ⟫ = ⟪ Pz , (λ c csc y⊆c → cl c csc (λ lt → y⊆c (eq→ x=y lt)) ) ⟫
+     eq← (Cl-cong {x} {y} x=y) ⟪ Pz , cl ⟫ = ⟪ Pz , (λ c csc x⊆c → cl c csc (λ lt → x⊆c (eq← x=y lt)) ) ⟫
      CF : HOD
-     CF = Replace (filter F) (λ x → Cl TP x  ) {P} record { ≤COD = λ {z} {y} lt → proj1 lt  } 
+     CF = Replace (filter F) (λ x → Cl TP x  ) {P} record { ≤COD = λ {z} {y} lt → proj1 lt ; ψ-eq = λ {x} {y} x=y → Cl-cong {x} {y} x=y } 
      CF⊆CS : CF ⊆ CS TP
      CF⊆CS {x} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef (CS TP) k) (sym x=ψz) (CS∋Cl TP (* z))
      --
@@ -352,8 +355,7 @@
         ufl07 : odef (filter F) x
         ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso))  ufl08  )
             (subst (λ k → odef (filter F) k) (sym &iso) az)
-            (subst (λ k → * z ⊆ k ) ? -- (trans (sym *iso) (sym (cong (*) x=ψz)) ) 
-               (x⊆Clx TP {* z} ufl09 ) ))
+            (λ xz → eq→ (==-sym (==-trans (o≡→== x=ψz) *iso )) (x⊆Clx TP {* z} ufl09 xz )))
      F∋sb  (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx))
         (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy))
             (λ z xz → fx→px (F∋sb sx) _ (eq← *iso (proj1 (eq→ *iso xz) )))
@@ -366,21 +368,20 @@
            begin
            x  ≡⟨ sym b ⟩
            o∅ ≡⟨ sym ord-od∅ ⟩
-           & od∅  ∎ ) ? -- (F∋sb (subst (λ k → Subbase k x) *iso sb ))
+           & od∅  ∎ ) (F∋sb  (sb⊆ (eq→ *iso) sb ))   -- (F∋sb (subst (λ k → Subbase k x) *iso sb ))
               ))  where open ≡-Reasoning
         ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
-     ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01)
-     ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01 {& P} ufl11  where
+     ufl10 : odef P (FIP.limit fip (λ lt → CF⊆CS (eq→ *iso lt) ) ufl01)
+     ufl10 = FIP.L∋limit fip (λ lt → CF⊆CS (eq→ *iso lt)) ufl01 {& P} ufl11  where
          ufl11 : odef (* (& CF)) (& P)
-         ufl11 = eq← *iso record { z = _ ; az  = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) ? ) ? -- (ClL TP)
-            ))   }
+         ufl11 = eq← *iso record { z = _ ; az  = F∋P ; x=ψz = sym (==→o≡ (==-trans (Cl-cong {* (& P)} {P} *iso) (ClL TP) )) }
      --
      -- so we have a limit
      --
      limit : Ordinal
-     limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01
+     limit = FIP.limit fip (λ lt →  CF⊆CS (eq→ *iso lt )) ufl01
      ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
-     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01
+     ufl02 = FIP.is-limit fip (λ lt → CF⊆CS (eq→ *iso lt)) ufl01
      --
      -- Neigbor of limit ⊆ Filter
      --
@@ -396,7 +397,7 @@
      ufl00 :  {v : Ordinal} → Neighbor TP limit v → filter F ∋ * v
      ufl00 {v} nei with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei ))
      ... | case1 fu = subst (λ k → odef (filter F) k) &iso
-       ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px)  fu (subst (λ k → u ⊆ k ) ? (Neighbor.u⊆v nei))) where
+       ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px)  fu (λ lt → eq← *iso (Neighbor.u⊆v nei lt))) where
          u = * (Neighbor.u nei)
          px : Power P ∋ * v
          px z vz = Neighbor.v⊆P nei (eq→ *iso vz )
@@ -405,10 +406,10 @@
          P\u : HOD
          P\u = P ＼ u
          P\u∋limit : odef P\u limit
-         P\u∋limit = eq→ *iso ( ufl02 (subst (λ k → odef k (& P\u)) ? ufl03 )) where
+         P\u∋limit = eq→ *iso ( ufl02 (eq← *iso ufl03 )) where
              ufl04 : & P\u ≡ & (Cl TP (* (& P\u)))
-             ufl04 = cong (&) (sym (trans (cong (Cl TP) ? ) ? ))
-                -- (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) )))))
+             ufl04 = ==→o≡ ( ==-sym ( ==-trans (Cl-cong {* (& P\u)} {P\u} *iso )
+                (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) ))) ))
              ufl03 : odef CF (& P\u )
              ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 }
          ¬P\u∋limit : ¬ odef P\u limit