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

diff -r d996fe8dd116 -r 8cbc3918d875 src/Topology.agda
--- a/src/Topology.agda	Sun Feb 26 01:19:24 2023 +0900
+++ b/src/Topology.agda	Sun Feb 26 11:16:32 2023 +0900
@@ -280,8 +280,9 @@
 -- Compact
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where
-   fin-e : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
-   fin-∪  : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
+   fin-e : Finite-∪ S o∅
+   fin-i : {x : Ordinal } → * x ⊆ S → Finite-∪ S x
+   fin-∪ : {x y : Ordinal } → Finite-∪ S x → Finite-∪ S y → Finite-∪ S (& (* x ∪ * y))
 
 record Compact  {L : HOD} (top : Topology L)  : Set n where
    field
@@ -301,11 +302,11 @@
    fip01 : {X : Ordinal } → (xcp : * X covers L) → (* o∅) covers L
    fip01 xcp = record { cover = λ Lx → ⊥-elim (fip02 Lx)  ; P∋cover = λ Lx → ⊥-elim (fip02 Lx)  ; isCover =  λ Lx → ⊥-elim (fip02 Lx) }
    fip00 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) o∅
-   fip00 {X} xo xcp = fin-e ( λ {x} 0x → ⊥-elim (¬x<0 (subst (λ k → odef k x) o∅≡od∅ 0x) ) )
+   fip00 {X} xo xcp = fin-e 
 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
    -- set of coset of X
    CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
-   CX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
+   CX {X} ox = & ( Replace (* X) (λ z → L ＼  z ))
    CCX : {X : Ordinal} → (os :  * X ⊆ OS top) → * (CX os) ⊆ CS top
    CCX {X} os {x} ox with subst (λ k → odef k x) *iso ox
    ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06  ⟫ where --  x ≡ & (L ＼ * z)
@@ -329,11 +330,11 @@
    --
    record CFIP (X x : Ordinal) : Set n where
       field
-         is-CS : * x ⊆ Replace' (* X) (λ z xz → L ＼ z)
+         is-CS : * x ⊆ Replace (* X) (λ z → L ＼ z)
          sx :  Subbase (* x)  o∅
    Cex : (X : Ordinal ) → HOD
-   Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace' (* X) (λ z xz → L ＼ z))) ; <odmax = fip05 } where
-       fip05 :  {y : Ordinal} →   CFIP X y → y o< osuc (& (Replace' (* X) (λ z xz → L ＼ z)))
+   Cex X = record { od = record { def = λ x → CFIP X x } ; odmax = osuc (& (Replace (* X) (λ z → L ＼ z))) ; <odmax = fip05 } where
+       fip05 :  {y : Ordinal} →   CFIP X y → y o< osuc (& (Replace (* X) (λ z → L ＼ z)))
        fip05 {y} cf = subst₂ (λ j k → j o< osuc k ) &iso refl ( ⊆→o≤ ( CFIP.is-CS cf ) )
    fip00 : {X : Ordinal } → * X ⊆ OS top → * X covers L → ¬ ( Cex X =h= od∅ )
    fip00 {X} ox oc cex=0 = ⊥-elim (fip09 fip25 fip20) where
@@ -343,7 +344,7 @@
        ... | 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 (* (CX ox)) k) b sc } )) where
-           fip10 : * (CX ox) ⊆ Replace' (* X) (λ z xz → L ＼ z)
+           fip10 : * (CX ox) ⊆ Replace (* X) (λ z → 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) ) )))
@@ -366,13 +367,13 @@
    --
    -- this defines finite cover
    finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
-   finCover {X} ox oc = & ( Replace' (* (cex ox oc)) (λ z xz → L ＼  z ))
+   finCover {X} ox oc = & ( Replace (* (cex ox oc)) (λ z → L ＼  z ))
    -- create Finite-∪ from cex
    isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
    isFinite {X} xo xcp = fip30 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp)) where
-        fip30 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) →  Subbase (* x) y → Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼  z )))
+        fip30 : ( x y : Ordinal ) → * x ⊆ Replace (* X) (λ z → L ＼ z) →  Subbase (* x) y → Finite-∪ (* X) (& (Replace (* x) (λ z → L ＼  z )))
         fip30 x y x⊆cs (gi sb) = fip31 where
-            fip32 : Replace' (* x) (λ z xz → L ＼ z) ⊆ * X --  x⊆cs :* x ⊆ Replace' (* X) (λ z₁ xz → L ＼ z₁) , x=ψz : w ≡ & (L ＼ * z) , odef (* x) z
+            fip32 : Replace (* x) (λ z → L ＼ z) ⊆ * X 
             fip32 {w} record { z = z ; az = xz ; x=ψz = x=ψz } with x⊆cs xz
             ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
                fip34 : * z1 ⊆ L
@@ -385,12 +386,21 @@
                  & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
                  & (L ＼ * z) ≡⟨ sym x=ψz ⟩
                  w ∎ where open ≡-Reasoning
-            fip31 : Finite-∪ (* X) (& (Replace' (* x) (λ z xz → L ＼ z)))
-            fip31 = fin-e (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
+            --  x⊆cs :* x ⊆ Replace (* X) (λ z₁ xz → L ＼ z₁) , x=ψz : w ≡ & (L ＼ * z) , odef (* x) z
+            fp38 : Subbase (* x) y 
+            fp38 = gi sb
+            fp35 : odef (* x) y
+            fp35 = sb
+            fp36 : odef (Replace (* X) (λ z → L ＼ z)) y
+            fp36 = x⊆cs sb
+            fp37 : odef (* X) (& (L ＼ * y))
+            fp37 = ?
+            fip31 : Finite-∪ (* X) (& (Replace (* x) (λ z → L ＼ z)))
+            fip31 = fin-i (subst (λ k → k ⊆ * X ) (sym *iso) fip32 )
         fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = fip35 where
-            fip35 : Finite-∪ (* X) (& (Replace' (* x) (λ z₁ xz → L ＼ z₁)))
+            fip35 : Finite-∪ (* X) (& (Replace (* x) (λ z₁ → L ＼ z₁)))
             fip35 = subst (λ k → Finite-∪ (* X) k)
-               (cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace' (* x) (λ z₁ xz → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _  x⊆cs sy)  (fip30 _ _ x⊆cs sz) )
+               (cong (&) (subst (λ k → (k ∪ k ) ≡ (Replace (* x) (λ z₁ → L ＼ z₁)) ) (sym *iso) x∪x≡x )) ( fin-∪ (fip30 _ _  x⊆cs sy)  (fip30 _ _ x⊆cs sz) )
    -- is also a cover
    isCover1 : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → * (finCover xo xcp) covers L
    isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L)
@@ -413,13 +423,13 @@
             fip47 {x} Lab with  fip45 {L} {a} {b} Lab
             ... | case1 La = isCover ca La
             ... | case2 Lb = isCover cb Lb
-        fip40 : ( x y : Ordinal ) → * x ⊆ Replace' (* X) (λ z xz → L ＼ z) →  Subbase (* x) y
-           → (Replace' (* x) (λ z xz → L ＼  z )) covers (L ＼ * y )
-        fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → L ＼ z)) covers ( L ＼ k ) ) (sym *iso)
+        fip40 : ( x y : Ordinal ) → * x ⊆ Replace (* X) (λ z → L ＼ z) →  Subbase (* x) y
+           → (Replace (* x) (λ z → L ＼  z )) covers (L ＼ * y )
+        fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace (* x) (λ z → L ＼ z)) covers ( L ＼ k ) ) (sym *iso)
           ( fip43 {_} {L} {* a} {* b} fip41 fip42 ) where
-            fip41 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * a)
+            fip41 : Replace (* x) (λ z → L ＼ z) covers (L ＼ * a)
             fip41 = fip40 x a x⊆r sa
-            fip42 : Replace' (* x) (λ z xz → L ＼ z) covers (L ＼ * b)
+            fip42 : Replace (* x) (λ z → L ＼ z) covers (L ＼ * b)
             fip42 = fip40 x b x⊆r sb
         fip40 x y x⊆r (gi sb) with x⊆r sb
         ... | record { z = z ; az = az ; x=ψz = x=ψz } = record { cover = fip51 ; P∋cover = fip53 ; isCover = fip50 }where
@@ -435,7 +445,7 @@
                 L ＼ ( L ＼ * z ) ≡⟨ cong (λ k → L ＼ k) (sym *iso)  ⟩
                 L ＼ * ( & ( L ＼ * z )) ≡⟨ cong (λ k → L ＼ * k) (sym x=ψz)  ⟩
                 L ＼ * y ∎  where open ≡-Reasoning
-            fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace' (* x) (λ z₁ xz → L ＼ z₁)) z
+            fip53 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (Replace (* x) (λ z₁ → L ＼ z₁)) z
             fip53 {w} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where
                fip54 : z ≡ & ( L ＼ * y )
                fip54 = begin
@@ -455,7 +465,7 @@
 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
    -- set of coset of X
    OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
-   OX {X} ox = & ( Replace' (* X) (λ z xz → L ＼  z ))
+   OX {X} ox = & ( Replace (* X) (λ z → L ＼  z ))
    OOX : {X : Ordinal} → (cs :  * X ⊆ CS top) → * (OX cs) ⊆ OS top
    OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox
    ... | record { z = z ; az = az ; x=ψz = x=ψz } =  subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01))  where
@@ -477,7 +487,8 @@
           fp01 : Ordinal
           fp01 = Compact.finCover compact (OOX CX) cov
           fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) )
-          fp02 t (fin-e t⊆OX ) = gi fp03 where
+          fp02 t fin-e = gi ?
+          fp02 t (fin-i tx ) = 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
diff -r d996fe8dd116 -r 8cbc3918d875 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Feb 26 01:19:24 2023 +0900
+++ b/src/Tychonoff.agda	Sun Feb 26 11:16:32 2023 +0900
@@ -156,7 +156,7 @@
      -- take closure of given filter elements
      --
      CF : HOD
-     CF = Replace' (filter F) (λ x fx → Cl TP x  )
+     CF = Replace (filter F) (λ x → Cl TP x  )
      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)) 
      --