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

diff -r 1925debf28bb -r 33116eb3abd1 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Mon Jul 01 16:37:12 2024 +0900
+++ b/src/Tychonoff.agda	Mon Jul 01 18:15:45 2024 +0900
@@ -134,18 +134,26 @@
    --   if 0 < X then 0 < x ∧ P ∋ xfrom fip
    --   if 0 ≡ X then ¬ odef X x
    fip03 {X} CX fip {x} xx with trio< o∅ X
-   ... | tri< 0<X ¬b ¬c = ? where -- ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso)
-        -- ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx))  xe ))) where
+   ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (eq← fip01 fip00) ) where
       0<x : o∅ o< x
       0<x = fip (gi xx )
       e : HOD  -- we have an element of x
       e = minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
       xe : odef (* x) (& e)
       xe = x∋minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
-   ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
-           * X ≡⟨ cong (*) (sym 0=X) ⟩
-           * o∅ ≡⟨ ? ⟩ --  o∅≡od∅ ⟩
-           od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
+      fip00 : odef P (& e)
+      fip00 = cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx))  xe 
+      fip01 : od∅ =h= P
+      fip01 = begin
+         od∅ ≈⟨ ==-sym o∅==od∅ ⟩
+         * o∅ ≈⟨ ==-sym (o≡→== P=0)  ⟩
+         * (& P) ≈⟨ *iso  ⟩
+         P ∎ where
+             open EqHOD ==-Setoid
+   ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋  (eq→ ( begin
+           * X ≈⟨ o≡→== (sym 0=X) ⟩
+           * o∅ ≈⟨ o∅==od∅ ⟩
+           od∅ ∎  ) (subst (λ k → odef (* X) k ) (sym &iso) xx )))  where open EqHOD ==-Setoid
    ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit =  uf01 } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
@@ -167,12 +175,12 @@
           Xe = x∋minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
           nn01 = minimal (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) )
           nn02 : * (& (nc 0<X CSX fip)) ⊆ P
-          nn02 = ? -- subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) )
+          nn02 lt = cs⊆L TP (CSX Xe ) (eq→ *iso lt )
 
      0<PP : o∅ o< & (Power P)     -- Power P contaisn od∅, so it is not empty
      0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where
           nn00 : odef (Power P) o∅
-          nn00 x lt with subst (λ k → odef k x) ? lt -- o∅≡od∅ lt
+          nn00 x lt with eq→ o∅==od∅ lt
           ... | x<0 = ⊥-elim ( ¬x<0 x<0)
      --
      -- FIP defines a filter
@@ -181,19 +189,19 @@
      F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
          f1 :  {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
          f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q =
-                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = ? -- subst (λ k → k ⊆ P) (sym *iso) f10 
-                          ; x⊆u = λ {z} xp → ? } where
-                            -- subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } where
+                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = λ lt → f10 (eq→ *iso lt) 
+                          ; x⊆u = λ {z} xp → eq← *iso (p⊆q (eq→ *iso (x⊆p xp))) } where
               f10 : q ⊆ P
               f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx  ))
          f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
          f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where
               p∩q⊆p : * (& (p ∩ q)) ⊆ P
-              p∩q⊆p {x} pqx = ? -- subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
+              p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq  (eq→ *iso (subst (λ k → odef (* (& (p ∩ q))) k ) (sym &iso) pqx )))
               Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq)
               xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
               sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
-              sbpq = ? -- subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
+              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