# HG changeset patch
# User kono
# Date 1677457595 -28800
# Node ID d969fc17d049cb852b81d7a1cc8e9dcc5c09f3af
# Parent  e110b56d8cbe08e7d77cf55eb06f41dc25aff28c
fix FIP again

diff -r e110b56d8cbe -r d969fc17d049 src/Topology.agda
--- a/src/Topology.agda	Mon Feb 27 07:29:11 2023 +0800
+++ b/src/Topology.agda	Mon Feb 27 08:26:35 2023 +0800
@@ -264,15 +264,20 @@
 
 -- Finite Intersection Property
 
+data Finite-∩ (S : HOD) : Ordinal → Set n where
+   fin-e : Finite-∩ S o∅
+   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 FIP {L : HOD} (top : Topology L) : Set n where
    field
        limit : {X : Ordinal } → * X ⊆ CS top
-          →       ( { x : Ordinal } → Subbase (* X) x → o∅ o< x ) →  Ordinal
+          →       ( { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x ) →  Ordinal
        is-limit : {X : Ordinal } → (CX : * X ⊆ CS top )
-          → ( fip :  { x : Ordinal } → Subbase (* X) x → o∅ o< x )
+          → ( fip :  { x : Ordinal } → Finite-∩ (* X) x → o∅ o< x )
           →  {x : Ordinal } → odef (* X) x → odef (* x) (limit CX fip)
    L∋limit  : {X : Ordinal } → (CX : * X ⊆ CS top )
-          → ( fip : { x : Ordinal } → Subbase (* X) x → o∅ o< x )
+          → ( fip : { x : Ordinal } → Finite-∩ (* 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)
@@ -328,18 +333,18 @@
    --     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 →  Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅
+   finCoverBase {X} ox oc with ODC.p∨¬p O (Finite-∩ (Replace (* X) (λ z → L ＼ z)) o∅)
    ... | case1 sb = sb
    ... | case2 ¬sb = ⊥-elim (fip09 fip25 fip20) where
        fip09 : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
        fip09 {z} Lz nc  =  nc ( P∋cover oc Lz  ) (subst (λ k → odef (* (cover oc Lz)) k) refl (isCover oc _ ))
        -- CX is finite intersection
-       fip02 : {x : Ordinal} → Subbase (* (CX ox)) x → o∅ o< x
+       fip02 : {x : Ordinal} → Finite-∩ (* (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 (¬sb (subst₂ (λ j k → Subbase j k ) *iso b sc )) 
+       ... | tri≈ ¬a b ¬c  = ⊥-elim (¬sb (subst₂ (λ j k → Finite-∩ j k ) *iso b sc )) 
        -- 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)
@@ -352,9 +357,10 @@
            fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
            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 ) , ( L ＼ * x  )
-   finCoverSet {X} x∩y (g∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy 
+   finCoverSet : {X : Ordinal } → (x : Ordinal) →  Finite-∩ (Replace (* X) (λ z → L ＼ z)) x → HOD
+   finCoverSet {X} x fin-e  =  ?
+   finCoverSet {X} x (fin-i rx) =  ( L ＼ * x ) , ( L ＼ * x  )
+   finCoverSet {X} x∩y (fin-∩ {x} {y} sx sy) = finCoverSet {X} x sx ∪ finCoverSet {X} y sy 
    --
    -- this defines finite cover
    finCover :  {X : Ordinal} → * X ⊆ OS top → * X covers L → Ordinal
@@ -362,8 +368,9 @@
    -- create Finite-∪ from cex
    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) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 rx)) where
+        fip60 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
+        fip60 x fin-e = ?
+        fip60 x (fin-i rx) = subst (λ k → Finite-∪ (* X) k) fip62 (fin-i (fip61 ? )) 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 ) ))
@@ -377,7 +384,7 @@
                  & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
                  & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
                  & (L ＼ * x ) ∎ where open ≡-Reasoning
-        fip60 x∩y (g∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx)  (fip60 y sy)  ) where
+        fip60 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → Finite-∪ (* X) k) fip62 ( fin-∪ (fip60 x sx)  (fip60 y sy)  ) where
                fip62 : & (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡ & (finCoverSet x sx ∪ finCoverSet y sy)
                fip62 = cong (&) ( begin
                   (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ *iso *iso ⟩ 
@@ -386,14 +393,21 @@
    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 (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
+        fip70 : (x : Ordinal) → (sb : Finite-∩ (Replace (* X) (λ z → L ＼ z)) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
+        fip70 x fin-e  = ?
+        fip70 x (fin-i rx) = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } 
+        fip70 x∩y (fin-∩ {x} {y} sx sy) = subst (λ k → finCoverSet (& (* x ∩ * y)) ? covers
+              (L ＼ k)) (sym *iso) ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) 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  ⟫
+            ... | no ¬bx = case2 ⟪ proj1 Lab , subst (λ k → ¬ ( odef b k)) &iso ¬bx  ⟫ 
+            fip71 : {a b c : HOD} → a covers c →  (a ∪ b) covers c
+            fip71 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case1 (P∋cover cov lt) 
+               ; isCover = isCover cov } 
+            fip72 : {a b c : HOD} → a covers c →  (b ∪ a) covers c
+            fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) 
+               ; isCover = isCover cov } 
             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
@@ -428,7 +442,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 : {x : Ordinal} → Subbase (* X) x → o∅ o< x) 
+   has-intersection : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* 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
@@ -439,12 +453,12 @@
       no-cover cov = ⊥-elim ( ? ) where
           fp01 : Ordinal
           fp01 = Compact.finCover compact (OOX CX) cov
-          fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Subbase (* X) (& ( L ＼ * t ) )
-          fp02 t fin-e = gi ?
-          fp02 t (fin-i tx ) = gi fp03 where
+          fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → Finite-∩ (* X) (& ( L ＼ * t ) )
+          fp02 t fin-e = ?
+          fp02 t (fin-i tx ) = ? 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
+          fp02 t (fin-∪ {tx} {ty} x y ) = subst (λ k → Finite-∩ (* X) k ) fp04 ( fin-∩ (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
@@ -497,14 +511,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 : {x : Ordinal} → Subbase (* X) x → o∅ o< x) 
+   limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Finite-∩ (* 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 : {x : Ordinal} → Subbase (* X) x → o∅ o< x)
+            (fip : {x : Ordinal} → Finite-∩ (* 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 )