# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677341964 -32400
# Node ID d996fe8dd116e4d60bb2270434ce779e5a4a2c3f
# Parent  ffe5bc98f9d1ea254e8c0082431bdfb38d880f34
...

diff -r ffe5bc98f9d1 -r d996fe8dd116 src/Topology.agda
--- a/src/Topology.agda	Sat Feb 25 23:39:34 2023 +0900
+++ b/src/Topology.agda	Sun Feb 26 01:19:24 2023 +0900
@@ -267,12 +267,12 @@
 record FIP {L : HOD} (top : Topology L) : Set n where
    field
        limit : {X : Ordinal } → * X ⊆ CS top
-          →       ( { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x ) →  Ordinal
+          →       ( { x : Ordinal } → Subbase (* X) x → o∅ o< x ) →  Ordinal
        is-limit : {X : Ordinal } → (CX : * X ⊆ CS top )
-          → ( fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x )
+          → ( fip :  { x : Ordinal } → Subbase (* X) x → o∅ o< x )
           →  {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip)
    L∋limit  : {X : Ordinal } → (CX : * X ⊆ CS top )
-          → ( fip : { C : Ordinal  } { x : Ordinal } → * C ⊆ * X → Subbase (* C) x → o∅ o< x )
+          → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x )
           →  {x : Ordinal } → odef (* X) x
           →  odef L (limit CX fip)
    L∋limit {X} CX fip {x} xx = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX xx)) (is-limit CX fip xx)
@@ -338,13 +338,13 @@
    fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ )
    fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where
        -- CX is finite intersection
-       fip02 : {C x : Ordinal} → * C ⊆ * (CX ox) → Subbase (* C) x → o∅ o< x
-       fip02 {C} {x} C<CX sc with trio< x o∅
+       fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x
+       fip02 {x} sc with trio< x o∅
        ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
        ... | tri> ¬a ¬b c = c
-       ... | tri≈ ¬a b ¬c  = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* C) k) b sc } )) where
-           fip10 : * C ⊆ Replace' (* X) (λ z xz → L ＼ z)
-           fip10 {w} cw = subst (λ k → odef k w) *iso ( C<CX cw )
+       ... | tri≈ ¬a b ¬c  = ⊥-elim (¬x<0 ( _==_.eq→ cex=0 record { is-CS = fip10 ; sx = subst (λ k → Subbase (* (CX ox)) k) b sc } )) where
+           fip10 : * (CX ox) ⊆ Replace' (* X) (λ z xz → L ＼ z)
+           fip10 {w} cw = subst (λ k → odef k w) *iso cw 
        -- we have some intersection because L is not empty (if we have an element of L, we don't need choice)
        fip26 : odef (* (CX ox))    (& (L ＼  * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )))
        fip26 = subst (λ k → odef k (& (L ＼  * ( cover oc ( ODC.x∋minimal O L (0<P→ne 0<L) ) )) )) (sym *iso)
@@ -465,7 +465,7 @@
    --   if all finite intersection of X contains something, 
    --   there is no finite cover. From Compactness, (OX X) is not a cover of L ( contraposition of Compact)
    --     it means there is a limit
-   has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
+   has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) 
       → o∅ o< X  →  ¬ (  Intersection (* X) =h= od∅ )
    has-intersection {X} CX fip 0<X i=0 =  ⊥-elim ( ¬x<0 {NC.x not-covered} ( eq→ i=0 ⟪ fp06 , fp05  ⟫ )) where
       fp07 : HOD  -- we have an element of X
@@ -473,15 +473,27 @@
       fp08 : odef (* X) (& fp07)
       fp08 = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
       no-cover : ¬ ( (* (OX CX)) covers L ) 
-      no-cover cov = ⊥-elim ( o<¬≡ ? (fip (λ x → x) (fp02 (Compact.isFinite compact (OOX CX) cov)))  ) where
+      no-cover cov = ⊥-elim ( ? ) where
           fp01 : Ordinal
           fp01 = Compact.finCover compact (OOX CX) cov
-          int : HOD
-          int = Replace (* fp01) (λ x → L ＼ x)
-          fp02 : Finite-∪ (* (OX CX)) fp01 → Subbase (* X) (& (Intersection (Replace (* fp01) (λ x → L ＼ x))))
-          fp02 = ?
-          fp03 : * (& (Replace (* fp01) (λ x → L ＼ x))) ⊆ * X
-          fp03 = ?
+          fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) )
+          fp02 t (fin-e t⊆OX ) = gi fp03 where
+              fp03 :  odef (* X) (& (L ＼ * t))
+              fp03 = ?
+          fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (fp02 tx x)  (fp02 ty y ) ) where
+              fp04 :  & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
+              fp04 = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
+                  fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
+                  fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt
+                  ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫  where
+                        fp06 : ¬ odef (* tx ∪ * ty) x 
+                        fp06 (case1 tx) = ¬tx tx
+                        fp06 (case2 ty) = ¬ty ty
+                  fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x
+                  fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt
+                  ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) 
+                         ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty))  ⟫ ⟫ 
+
       record  NC : Set n where   -- x is not covered 
         field
            x : Ordinal
@@ -494,7 +506,7 @@
           coverSet {x} Lx = record { od = record { def = λ y → odef (* X) y ∧ odef (L ＼ * y) x } ; odmax = X 
              ; <odmax = λ {x} lt → subst (λ k → x o< k) &iso ( odef< (proj1 lt)) }
           fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ )
-          fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; Lx = Lx ; yx = fp19 } ) where
+          fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where
              fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x
              fp19 {y} Xy with ∨L＼X {L} {* y} {x} Lx
              ... | case1 yx = yx
@@ -521,14 +533,14 @@
          & (* (NC.x not-covered)) <⟨ c<→o< (subst₂ (λ j k → odef j k ) *iso (sym &iso) (NC.yx not-covered fp08)) ⟩
          & fp07  <⟨ c<→o< fp08 ⟩
          & (* X) ∎ where open o≤-Reasoning O
-   limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x) 
+   limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) 
       → Ordinal
    limit {X} CX fip with trio< X o∅ 
    ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
    ... | tri≈ ¬a b ¬c = o∅
    ... | tri> ¬a ¬b c = & (ODC.minimal O (Intersection (* X)) ( has-intersection CX fip c))
    fip00 : {X : Ordinal} (CX : * X ⊆ CS top)
-            (fip : {C x : Ordinal} → * C ⊆ * X → Subbase (* C) x → o∅ o< x)
+            (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
             {x : Ordinal} → odef (* X) x → odef (* x) (limit CX fip )
    fip00 {X} CX fip {x} Xx with trio< X o∅
    ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
diff -r ffe5bc98f9d1 -r d996fe8dd116 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sat Feb 25 23:39:34 2023 +0900
+++ b/src/Tychonoff.agda	Sun Feb 26 01:19:24 2023 +0900
@@ -68,7 +68,7 @@
    fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
 ... | tri> ¬a ¬b 0<P = record { limit = limit ; is-limit = uf01 } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
-     fip {X} CSX = {u x : Ordinal} → * u ⊆ * X → Subbase (* u) x → o∅ o< x
+     fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
      N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
      N {X} CSX fp = record { od = record { def = λ u → FBase P X u } ; odmax = osuc (& P)
         ; <odmax = λ {x} lt → subst₂ (λ j k → j o< osuc k) &iso refl (⊆→o≤ (FBase.u⊆P lt))  }
@@ -162,7 +162,7 @@
      --
      -- it is set of closed set and has FIP ( F is proper )
      --
-     ufl01 : {C x : Ordinal} → * C ⊆ * (& CF) → Subbase (* C) x → o∅ o< x
+     ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x
      ufl01 = ?
      --
      -- so we have a limit
@@ -245,7 +245,7 @@
                  b∋z : odef nei1 z
                  b∋z = ?
                  bp : BaseP {P} TP Q z
-                 bp = record { b = ? ; op = ? ; prod = ? }
+                 bp = record { p = ? ; op = ? ; prod = ? }
                  neip : {p : Ordinal } → ( bp : BaseP TP Q p ) → * p ⊆ filter F 
                  neip = ?
                  il2 : * z ⊆ ZFP (Power P) (Power Q)