# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1673973804 -32400
# Node ID 8a071bf52407aebfbf1e080fdc440d42df6af929
# Parent  fe0129c407458b729c3b0c22b8491ef07d56f69f
Finite intersection property to Compact done

diff -r fe0129c40745 -r 8a071bf52407 src/BAlgebra.agda
--- a/src/BAlgebra.agda	Tue Jan 17 11:21:18 2023 +0900
+++ b/src/BAlgebra.agda	Wed Jan 18 01:43:24 2023 +0900
@@ -40,6 +40,25 @@
     lem1 : {x : Ordinal} → odef  od∅ x → odef (L ＼ L) x
     lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
 
+L＼Lx=x : { L x : HOD  } → x ⊆ L   → L ＼ ( L ＼ x ) ≡ x
+L＼Lx=x {L} {x} x⊆L = ==→o≡ ( record { eq→ = lem03 ; eq← = lem04 } ) where
+    lem03 :  {z : Ordinal} → odef (L ＼ (L ＼ x)) z → odef x z 
+    lem03 {z} ⟪ Lz , Lxz ⟫ with ODC.∋-p O x (* z)
+    ... | yes y = subst (λ k → odef x k ) &iso y 
+    ... | no n = ⊥-elim ( Lxz ⟪ Lz , ( subst (λ k → ¬ odef x k ) &iso n ) ⟫ )
+    lem04 :  {z : Ordinal} → odef x z → odef (L ＼ (L ＼ x)) z 
+    lem04 {z} xz with ODC.∋-p O L (* z)
+    ... | yes y = ⟪ subst (λ k → odef L k ) &iso y  , ( λ p → proj2 p xz )  ⟫
+    ... | no  n = ⊥-elim ( n (subst (λ k → odef L k ) (sym &iso) ( x⊆L xz) ))
+     
+L＼0=L : { L  : HOD  } → L ＼ od∅ ≡ L 
+L＼0=L {L} = ==→o≡ ( record { eq→ = lem05 ; eq← = lem06 } ) where
+    lem05 : {x : Ordinal} → odef (L ＼ od∅) x → odef L x
+    lem05 {x} ⟪ Lx , _ ⟫ = Lx
+    lem06 : {x : Ordinal} → odef L x → odef (L ＼ od∅) x
+    lem06 {x} Lx = ⟪ Lx , (λ lt → ¬x<0 lt)  ⟫
+
+
 [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 fe0129c40745 -r 8a071bf52407 src/ODUtil.agda
--- a/src/ODUtil.agda	Tue Jan 17 11:21:18 2023 +0900
+++ b/src/ODUtil.agda	Wed Jan 18 01:43:24 2023 +0900
@@ -56,6 +56,12 @@
       lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
       lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
 
+x∪x≡x : { A  : HOD  } → (A ∪ A) ≡ A 
+x∪x≡x {A} = ==→o≡ record { eq← = λ {x} lt → case1 lt ; eq→ =  lem00 } where
+    lem00 : {x : Ordinal} → odef A x ∨ odef A x → odef A x
+    lem00 {x} (case1 ax) = ax
+    lem00 {x} (case2 ax) = ax
+
 _＼_ : ( A B : HOD  ) → HOD
 A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
 
@@ -251,22 +257,13 @@
 -- ∋-irr : {X x : HOD} → (a b : X ∋ x ) → a ≡ b
 -- ∋-irr {X} {x} _ _ = refl
 --    is requed in
--- Replace∩ : {X P Q : HOD}  → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
---     → Replace' (P ∩ Q) (λ _ pq → ψ _ (P⊆X (proj1 pq ))) ≡ Replace' P (λ _ p → ψ _ (P⊆X p)) ∩ Replace' Q (λ _ q → ψ _ (Q⊆X q))
--- Replace∩ {X} {P} {Q} {ψ} P⊆X Q⊆X = ==→o≡ record { eq→ = lem04 ; eq← = ? } where
---     lem04 : {x : Ordinal} → OD.def (od (Replace' (P ∩ Q) (λ z pq → ψ z (P⊆X (proj1 pq)) ))) x
---        → OD.def (od (Replace' P (λ z p → ψ z (P⊆X p)) ∩ Replace' Q (λ z q → ψ z (Q⊆X q)))) x
---     lem04 {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪
---          record { z = _ ; az = proj1 az ; x=ψz = ? }  ,
---          record { z = _ ; az = proj2 az ; x=ψz = ? } ⟫
+Replace∩ : {X P Q : HOD}  → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
+    → ( {x : HOD} → (a b : X ∋ x ) → ψ x a ≡ ψ x b )
+    → (Replace' (P ∩ Q) (λ _ pq → ψ _ (P⊆X (proj1 pq ))))   ⊆ ( Replace' P (λ _ p → ψ _ (P⊆X p)) ∩ Replace' Q (λ _ q → ψ _ (Q⊆X q)))
+Replace∩ {X} {P} {Q} {ψ} P⊆X Q⊆X ψ-irr = lem04 where
+    lem04 : {x : Ordinal} → OD.def (od (Replace' (P ∩ Q) (λ z pq → ψ z (P⊆X (proj1 pq)) ))) x
+       → OD.def (od (Replace' P (λ z p → ψ z (P⊆X p)) ∩ Replace' Q (λ z q → ψ z (Q⊆X q)))) x
+    lem04 {x} record { z = z ; az = az ; x=ψz = x=ψz } = ⟪
+         record { z = _ ; az = proj1 az ; x=ψz = trans  x=ψz (cong (&)(ψ-irr _ _)) }  ,
+         record { z = _ ; az = proj2 az ; x=ψz = trans  x=ψz (cong (&)(ψ-irr _ _)) } ⟫
 
-Repl∪ψ : {X P Q : HOD}  → (ψ : (x : HOD) → X ∋ x → HOD) → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X ) → (x : HOD) → (P ∪ Q) ∋ x → HOD
-Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case1 p) = ψ _ (P⊆X p)
-Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X x (case2 q) = ψ _ (Q⊆X q)
-
-Replace∪ : {X P Q : HOD}  → {ψ : (x : HOD) → X ∋ x → HOD} → (P⊆X : P ⊆ X) → (Q⊆X : Q ⊆ X )
-    → Replace' (P ∪ Q) (Repl∪ψ {X} {P} {Q} ψ P⊆X Q⊆X) ≡ Replace' P (λ _ p → ψ _ (P⊆X p)) ∪ Replace' Q (λ _ q → ψ _ (Q⊆X q))
-Replace∪ {X} {P} {Q} {ψ} P⊆X Q⊆X = ==→o≡ record { eq→ = ? ; eq← = ? }
-
-
-
diff -r fe0129c40745 -r 8a071bf52407 src/Topology.agda
--- a/src/Topology.agda	Tue Jan 17 11:21:18 2023 +0900
+++ b/src/Topology.agda	Wed Jan 18 01:43:24 2023 +0900
@@ -281,9 +281,9 @@
          is-CS : * x ⊆ Replace' (* X) (λ z xz → 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 = ? } where
-       fip05 :  {y : Ordinal} → CFIP X y → y o< osuc (& L)
-       fip05 {y} cf = subst₂ (λ j k →  j o≤ k ) ? ? ( ⊆→o≤ ( CFIP.is-CS cf ))
+   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)))
+       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
        -- CX is finite intersection
@@ -321,16 +321,81 @@
    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 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 {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
+               fip34 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az1)) wz1
+               fip33 : z1 ≡ w
+               fip33 = begin
+                 z1 ≡⟨ sym &iso ⟩ 
+                 & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩ 
+                 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩ 
+                 & (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 ?
-        fip30 x yz x⊆cs (g∩ {y} {z} sy sz) = ?
+            fip31 = fin-e (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 = 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) )
    -- 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) ? ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where
+   isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) (sym *iso) (subst (λ k → L ＼ k ≡ L) (sym o∅≡od∅) L＼0=L) 
+     ( fip40 (cex xo xcp) o∅ (CFIP.is-CS (CXfip xo xcp)) (CFIP.sx (CXfip xo xcp))) where
         -- record { cover = λ {x} Lx → ?  ; P∋cover = ? ; isCover = ? }
+        fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪  (L ＼ b))
+        fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
+        ... | yes bx = case1 ⟪ proj1 Lab , (λ ax → proj2 Lab ⟪ ax , subst (λ k → odef b k) &iso bx ⟫ )  ⟫
+        ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx  ⟫
+        fip43 : {A L a b : HOD } → A covers (L ＼ a) → A covers (L ＼ b ) → A covers ( L ＼ ( a ∩ b ) )
+        fip43 {A} {L} {a} {b} ca cb = record { cover = fip44 ; P∋cover = fip46 ; isCover = fip47 } where
+            fip44 :  {x : Ordinal} → odef (L ＼ (a ∩ b)) x → Ordinal
+            fip44 {x} Lab with fip45 {L} {a} {b} Lab
+            ... | case1 La = cover ca La
+            ... | case2 Lb = cover cb Lb
+            fip46 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef A (fip44 lt)
+            fip46 {x} Lab with  fip45 {L} {a} {b} Lab
+            ... | case1 La = P∋cover ca La
+            ... | case2 Lb = P∋cover cb Lb
+            fip47 : {x : Ordinal} (lt : odef (L ＼ (a ∩ b)) x) → odef (* (fip44 lt)) x 
+            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 = ?
+        fip40 x .(& (* _ ∩ * _)) x⊆r (g∩ {a} {b} sa sb) = subst (λ k → (Replace' (* x) (λ z xz → 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 = fip40 x a x⊆r sa  
+            fip42 : Replace' (* x) (λ z xz → 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
+            fip51 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → Ordinal 
+            fip51 {w} Lyw = z 
+            fip52 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* X) z 
+            fip52 {w} Lyw = az 
+            fip55 : * z ⊆ L
+            fip55 {w} wz1 = os⊆L top (subst (λ k → odef (OS top) k) (sym &iso) (xo az)) wz1
+            fip56 : * z ≡ L ＼ * y
+            fip56 = begin
+                * z ≡⟨ sym (L＼Lx=x fip55 ) ⟩
+                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} Lyw = record { z = _ ; az = sb ; x=ψz = fip54 } where
+               fip54 : z ≡ & ( L ＼ * y )
+               fip54 = begin
+                 z ≡⟨ sym &iso ⟩
+                 & (* z) ≡⟨ cong (&) fip56 ⟩
+                 & (L ＼ * y )  
+                 ∎ where open ≡-Reasoning
+            fip50 : {w : Ordinal} (Lyw : odef (L ＼ * y) w) → odef (* z) w 
+            fip50 {w} Lyw = subst (λ k → odef k w ) (sym fip56) Lyw 
+
 
 
 -- some day