# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1685625317 -32400
# Node ID 37f28f4276611d9263802355d91b60b70b081506
# Parent  f29970636e017f98b5eb94b569a22b581c93fba9
...

diff -r f29970636e01 -r 37f28f427661 src/BAlgebra.agda
--- a/src/BAlgebra.agda	Thu Jun 01 20:33:20 2023 +0900
+++ b/src/BAlgebra.agda	Thu Jun 01 22:15:17 2023 +0900
@@ -72,6 +72,12 @@
     ... | case1 bx = bx
     ... | case2 ¬bx = ⊥-elim ( proj2 ( pba ⟪ A⊆P ax  , ¬bx ⟫ ) ax )
 
+RC＼ : {L : HOD} → RCod (Power (Union L)) (λ z → L ＼ z )
+RC＼ {L} = record { ≤COD = λ {x} lt z xz → lemm {x} lt z xz  } where
+    lemm : {x : HOD} → (L ＼ x) ⊆ Power (Union L )
+    lemm {x} ⟪ Ly , nxy ⟫ z xz = record { owner = _ ; ao = Ly ; ox = xz }
+
+
 [a-b]∩b=0 : { A B : HOD } → (A ＼ B) ∩ B ≡ od∅
 [a-b]∩b=0 {A} {B} = ==→o≡ record { eq← = λ lt → ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
      ; eq→ =  λ {x} lt → ⊥-elim (proj2 (proj1 lt ) (proj2 lt)) }
diff -r f29970636e01 -r 37f28f427661 src/PFOD.agda
--- a/src/PFOD.agda	Thu Jun 01 20:33:20 2023 +0900
+++ b/src/PFOD.agda	Thu Jun 01 22:15:17 2023 +0900
@@ -22,6 +22,7 @@
 open OD O
 open OD.OD
 open ODAxiom odAxiom
+open ODAxiom-ho< odAxiom-ho<
 import OrdUtil
 import ODUtil
 open Ordinals.Ordinals  O
diff -r f29970636e01 -r 37f28f427661 src/Topology.agda
--- a/src/Topology.agda	Thu Jun 01 20:33:20 2023 +0900
+++ b/src/Topology.agda	Thu Jun 01 22:15:17 2023 +0900
@@ -314,7 +314,7 @@
 ... | 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 → L ＼  z ))
+   CX {X} ox = & ( Replace (* X) (λ z → L ＼  z ) RC＼ )
    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)
@@ -336,8 +336,8 @@
    --     then some finite Intersection of (CX X) contains nothing ( contraposition of FIP .i.e. CFIP)
    --     it means there is a finite cover
    --
-   finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L →  Subbase (Replace (* X) (λ z → L ＼ z)) o∅
-   finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z)) o∅)
+   finCoverBase : {X : Ordinal } → * X ⊆ OS top → * X covers L →  Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) o∅
+   finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) o∅)
    ... | case1 sb = sb
    ... | case2 ¬sb = ⊥-elim (¬¬cover fip25 fip20) where
        ¬¬cover : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
@@ -361,7 +361,7 @@
            fip21 : odef (L ＼ * y) ( FIP.limit fip (CCX ox) fip02 )
            fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) *iso ( FIP.is-limit fip (CCX ox) fip02 fip22 )
    -- create HOD from Subbase ( finite intersection )
-   finCoverSet : {X : Ordinal } → (x : Ordinal) →  Subbase (Replace (* X) (λ z → L ＼ z)) x → HOD
+   finCoverSet : {X : Ordinal } → (x : Ordinal) →  Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x → HOD
    finCoverSet {X} x (gi rx) =  ( L ＼ * x ) , ( L ＼ * x  )
    finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy 
    --
@@ -371,11 +371,11 @@
    -- create Finite-∪ from finCoverSet
    isFinite : {X : Ordinal} (xo : * X ⊆ OS top) (xcp : * X covers L) → Finite-∪ (* X) (finCover xo xcp)
    isFinite {X} xo xcp = fip60 o∅ (finCoverBase xo xcp) where
-        fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
+        fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
         fip60 x (gi rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where
            fip62 : & (* (& (L ＼ * x)) , * (& (L ＼ * x))) ≡ & ((L ＼ * x) , (L ＼ * x))
            fip62 = cong₂ (λ j k → & (j , k )) *iso *iso
-           fip61 : odef (Replace (* X) (_＼_ L)) x → odef (* X) ( & ((L ＼ * x ) ))
+           fip61 : odef (Replace (* X) (_＼_ L) RC＼ ) x → odef (* X) ( & ((L ＼ * x ) ))
            fip61 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
                fip34 : * z1 ⊆ L
                fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
@@ -395,7 +395,7 @@
    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) 
      (fip70 o∅ (finCoverBase xo xcp)) where
-        fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
+        fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
         fip70 x (gi rx) = fip73 where
             fip73 : ((L ＼ * x) , (L ＼ * x)) covers (L ＼ * x)   -- obvious
             fip73 = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl 
@@ -454,7 +454,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 → L ＼  z ))
+   OX {X} ox = & ( Replace (* X) (λ z → L ＼  z ) RC＼)
    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
diff -r f29970636e01 -r 37f28f427661 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Thu Jun 01 20:33:20 2023 +0900
+++ b/src/Tychonoff.agda	Thu Jun 01 22:15:17 2023 +0900
@@ -34,7 +34,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
@@ -190,11 +190,11 @@
      --    otherwise the check requires a minute
      --
      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)
+     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 it has a limit as a limit of FIP
      --
@@ -283,7 +283,7 @@
      -- take closure of given filter elements
      --
      CF : HOD
-     CF = Replace (filter F) (λ x → Cl TP x  )
+     CF = Replace (filter F) (λ x → Cl TP x  ) {P} record { ≤COD = λ {z} {y} lt → proj1 lt  } 
      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))
      --
@@ -424,7 +424,7 @@
          isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q
          isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q
          fx→px : {x : HOD } → filter F ∋ x → HOD
-         fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) ))
+         fx→px {x} fx = Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) {P} record { ≤COD = λ {x} lt {y} ly → ? }
          fx→px1 : {p : HOD } {q : Ordinal } → odef Q q → (fp : filter F ∋  ZFP p Q ) → fx→px fp ≡ p
          fx→px1 {p} {q} qq fp = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
              ty21 : {a b : Ordinal } → (pz : odef p a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >)))
@@ -453,7 +453,7 @@
 
          --  Projection of F
          FPSet : HOD
-         FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))
+         FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )) ? ) ?
 
          --  Projection ⁻¹  F (which is in F) is in FPSet
          FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋  ZFP q Q → FPSet ∋ q
@@ -464,15 +464,15 @@
               ty11 {y} {xy}  = cong (λ k → * (zπ1 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where
                  a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy
                  b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)
-              ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q
+              ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ? ≡ q
               ty10 = begin
-                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy)))
+                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ?
                      ≡⟨
-                  cong (λ k → Replace' (* (& (ZFP q Q))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy}))))
+                  cong (λ k → Replace' (* (& (ZFP q Q))) k ? ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy})))) 
                       ⟩
-                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  )))
-                     ≡⟨ Replace'-iso _  ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ⟩
-                  Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ≡⟨ refl ⟩
+                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  ))) ?
+                     ≡⟨ Replace'-iso _  ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ? ⟩
+                  Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ?  ≡⟨ refl ⟩
                   fx→px fq ≡⟨ fx→px1 aq fq  ⟩
                   q ∎ where open ≡-Reasoning
          FPSet⊆PP :  FPSet  ⊆ Power P
@@ -484,7 +484,7 @@
          X=F1 x p fx = & p ≡ & (Replace' (* x) (λ y xy →
            * (zπ1 (f⊆L F
              (subst (odef (filter F)) (sym &iso) fx)
-             (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))))
+             (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))) ? )
          x⊆pxq : {x : Ordinal} {p : HOD} (fx : odef (filter F) x) → X=F1 x p fx → * x ⊆ ZFP p Q
          x⊆pxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
          ... | ab-pair {a} {b} pw qw = ab-pair ty08 qw where
@@ -569,7 +569,7 @@
          FPSet⊆F : {x : Ordinal } → odef FPSet x →  odef (filter F) (& (ZFP (* x) Q))
          FPSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where
              Rx : HOD
-             Rx = Replace' (* z) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy)))
+             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 b )) where
                  a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw) 
@@ -610,7 +610,7 @@
          isQ→PxQ : {x : HOD} → (x⊆Q : x ⊆ Q ) → ZFP P x  ⊆ ZFP P Q
          isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q)
          fx→qx : {x : HOD } → filter F ∋ x → HOD
-         fx→qx {x} fx = Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) ))
+         fx→qx {x} fx = Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) ?
          fx→qx1 : {q : HOD } {p : Ordinal } → odef P p → (fq : filter F ∋  ZFP P q ) → fx→qx fq ≡ q
          fx→qx1 {q} {p} qq fq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
              ty21 : {a b : Ordinal } → (qz : odef q b) → (pz : odef P a) → ZFProduct P Q (& (* (& < * a , * b >)))
@@ -637,7 +637,7 @@
                     * x ≡⟨ sym (cong (*) (ty32 qx qq )) ⟩
                     * (zπ2 (F⊆pxq fq (subst (odef (ZFP P q)) (sym &iso) (ab-pair qq qx )))) ∎ where open ≡-Reasoning
          FQSet : HOD
-         FQSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )))
+         FQSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ2 (F⊆pxq fx xy) )) ? ) ?
          FQSet∋zpq : {q : HOD} → q ⊆ Q → filter F ∋  ZFP P q → FQSet ∋ q
          FQSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where
               -- brain damaged one
@@ -646,15 +646,15 @@
               ty11 {y} {xy}  = cong (λ k → * (zπ2 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where
                  a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy
                  b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)
-              ty10 : Replace' (* (& (ZFP P q ))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q
+              ty10 : Replace' (* (& (ZFP P q ))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ?  ≡ q
               ty10 = begin
-                  Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy)))
+                  Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ?
                      ≡⟨
-                  cong (λ k → Replace' (* (& (ZFP P q ))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy}))))
+                  cong (λ k → Replace' (* (& (ZFP P q ))) k ? ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy}))))
                       ⟩
-                  Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  )))
-                     ≡⟨ Replace'-iso _  ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ⟩
-                  Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ≡⟨ refl ⟩
+                  Replace' (* (& (ZFP P q))) (λ y xy → * (zπ2 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  ))) ?
+                     ≡⟨ Replace'-iso _  ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ? ⟩
+                  Replace' (ZFP P q ) ( λ y xy → * (zπ2 (F⊆pxq fq xy) )) ?  ≡⟨ refl ⟩
                   fx→qx fq ≡⟨ fx→qx1 ap fq  ⟩
                   q ∎ where open ≡-Reasoning
          FQSet⊆PP :  FQSet  ⊆ Power Q
@@ -666,7 +666,7 @@
          X=F2 x q fx = & q ≡ & (Replace' (* x) (λ y xy →
            * (zπ2 (f⊆L F
              (subst (odef (filter F)) (sym &iso) fx)
-             (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))))
+             (& y) (subst (λ k → OD.def (HOD.od k) (& y)) (sym *iso) xy)))) ? )
          x⊆qxq : {x : Ordinal} {q : HOD} (fx : odef (filter F) x) → X=F2 x q fx → * x ⊆ ZFP P q
          x⊆qxq {x} {p} fx x=ψz {w} xw with F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fx) xw
          ... | ab-pair {a} {b} pw qw = ab-pair pw ty08 where
@@ -750,7 +750,7 @@
          FQSet⊆F : {x : Ordinal } → odef FQSet x →  odef (filter F) (& (ZFP P (* x) ))
          FQSet⊆F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F ty80 (subst (λ k → odef (filter F) k) (sym &iso) az) ty71 where
              Rx : HOD
-             Rx = Replace' (* z) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy)))
+             Rx = Replace' (* z) (λ y xy → * (zπ2 (F⊆pxq (subst (odef (filter F)) (sym &iso) az) xy))) ?
              PxRx∋z : * z ⊆ ZFP P Rx  
              PxRx∋z {w} zw = subst (λ k → ZFProduct P Rx k ) ty70 ( ab-pair (zp1 b) record { z = w ; az = zw ; x=ψz = refl } ) where
                  a = F⊆pxq (subst (odef (filter F)) (sym &iso) az) (subst (odef (* z)) (sym &iso) zw)