# HG changeset patch
# User kono
# Date 1677454151 -28800
# Node ID e110b56d8cbe08e7d77cf55eb06f41dc25aff28c
# Parent  0201827b08ac8aaefc32cafcb0a7f0f1d60f3976
...

diff -r 0201827b08ac -r e110b56d8cbe src/Topology.agda
--- a/src/Topology.agda	Sun Feb 26 18:30:23 2023 +0900
+++ b/src/Topology.agda	Mon Feb 27 07:29:11 2023 +0800
@@ -281,7 +281,7 @@
 
 data Finite-∪ (S : HOD) : Ordinal → Set n where
    fin-e : Finite-∪ S o∅
-   fin-i : {x : Ordinal } → odef S x → Finite-∪ S x
+   fin-i : {x : Ordinal } → odef S x  → Finite-∪ S (& ( * x , * 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
@@ -353,7 +353,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 )
    finCoverSet : {X : Ordinal } → (x : Ordinal) →  Subbase (Replace (* X) (λ z → L ＼ z)) x → HOD
-   finCoverSet {X} x (gi rx) = L ＼ * x 
+   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 
    --
    -- this defines finite cover
@@ -363,7 +363,9 @@
    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 (gi rx) = fin-i (fip61 rx) where
+        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 record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
                fip34 : * z1 ⊆ L
@@ -382,57 +384,30 @@
                   finCoverSet x sx ∪ finCoverSet y sy ∎ ) where open ≡-Reasoning
    -- 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) ? where
-        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 → 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 → L ＼ z) covers (L ＼ * a)
-            fip41 = fip40 x a x⊆r sa
-            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
-            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₁ → 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
+   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 (gi rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } 
+        fip70 x∩y (g∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) (g∩ sx sy) covers
+              (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} ? ? ) where
+            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
 
 open _==_