# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1677598654 -32400
# Node ID 0a88fcd5d1c98e7dd2485b32e5d1375b0fef4590
# Parent  e7c3bd9e7c3e20b0655db49d106da67222778511
... almost

diff -r e7c3bd9e7c3e -r 0a88fcd5d1c9 src/Topology.agda
--- a/src/Topology.agda	Tue Feb 28 22:33:13 2023 +0900
+++ b/src/Topology.agda	Wed Mar 01 00:37:34 2023 +0900
@@ -420,7 +420,11 @@
 Compact→FIP : {L : HOD} → (top : Topology L ) → Compact top  → FIP top
 Compact→FIP {L} top compact with trio< (& L) o∅
 ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
-... | tri≈ ¬a b ¬c = record { limit = ? ; is-limit = ? } 
+... | tri≈ ¬a b ¬c = record { limit = λ {X} CX fip → o∅ ; is-limit = λ {X} CX fip xx → ⊥-elim (fip000 CX xx)  }  where
+   fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ¬  odef (* X) x
+   fip000 {X} {x} CX xx = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) b)) o∅≡od∅ ) (sym &iso) 
+       ( cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) (CX xx))  ? ))
+   -- (subst (λ k → odef (CS top) k) (sym &iso) ( CX xx ) ) ))
 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
    -- set of coset of X
    OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
@@ -450,12 +454,19 @@
                sb : Subbase (* X) (& (L ＼ * i))
                not-t : (L ＼ * i) ⊆  (L ＼ Union ( * t ) )
           fp02 : (t : Ordinal) → Finite-∪ (* (OX CX)) t → SB t
-          fp02 t fin-e = record { i = & ( L  ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = ?  } where  
+          fp02 t fin-e = record { i = & ( L  ＼ fp07) ; sb = gi (subst (λ k → odef (* X) k) fp21 fp08) ; not-t = fp23  } where  
               fp22 : fp07 ⊆ L
               fp22 {x} lt =  cs⊆L top (CX fp08) lt 
               fp21 : & fp07 ≡ & (L ＼ * (& (L ＼ fp07)))
               fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼  k) (sym *iso)))
-          fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03  ; not-t = ? } where
+              fp23 : (L ＼ * (& (L ＼ fp07))) ⊆ (L ＼ Union (* o∅))
+              fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) (Own.ao lt )))) ⟫ 
+          fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03  ; not-t = fp24 } where
+              fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x))))
+              fp24 {y} ⟪ Lx , not ⟫  = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) (sym *iso) fp25  ⟫ where
+                   fp25 : ¬ odef (Union (* x , * x)) y
+                   fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox )
+                   fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) *iso ox )
               fp03 :  odef (* X) (& (L ＼ * x))
               fp03 with subst (λ k → odef k x ) *iso tx
               ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
@@ -468,7 +479,37 @@
                      & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
                      & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
                      & (L ＼ * x ) ∎ where open ≡-Reasoning
-          fp02 t (fin-∪ {tx} {ty} x y ) =  record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11  ; not-t = ? } where
+          fp02 t (fin-∪ {tx} {ty} x y ) =  record { i = & (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))) ; sb = fp11  ; not-t = fp35 } where
+              fp35 : (L ＼ * (& (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty))))
+              fp35 = subst₂ (λ j k →  (L ＼ j ) ⊆ (L ＼ Union k)) (sym *iso) (sym *iso) fp36  where
+                  fp40 : {z tz : Ordinal } → Finite-∪ (* (OX CX)) tz → odef (Union (* tz )) z → odef L z 
+                  fp40 {z} {.(Ordinals.o∅ O)} fin-e record { owner = owner ; ao = ao ; ox = ox } = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅  (sym &iso) ao ))
+                  fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (subst (λ k → odef (Union k) z) *iso uz)  where
+                       fp41 : (x : odef (* (OX CX)) w) → (uz : odef (Union (* w , * w)) z ) → odef L z
+                       fp41 x record { owner = .(& (* w)) ; ao = (case1 refl) ; ox = ox } = 
+                           os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox )
+                       fp41 x record { owner = .(& (* w)) ; ao = (case2 refl) ; ox = ox } = 
+                           os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) *iso ox )
+                  fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz with subst (λ k → odef (Union k) z ) *iso uz
+                  ... | record { owner = o ; ao = case1 x1o ; ox = oz } = fp40 ftx record { owner = o ; ao = x1o ; ox = oz } 
+                  ... | record { owner = o ; ao = case2 y1o ; ox = oz } = fp40 fty record { owner = o ; ao = y1o ; ox = oz } 
+                  fp36 : (L ＼  (* (SB.i (fp02 tx x)) ∪ * (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* tx ∪ * ty))
+                  fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where
+                      fp37 : ¬ odef (Union (* tx ∪ * ty)) z 
+                      fp37 record { owner = owner ; ao = (case1 ax) ; ox = ox } = not (case1 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
+                          fp38 : (L ＼  (* (SB.i (fp02 tx x)))) ⊆ (L ＼ Union (* tx))
+                          fp38 = SB.not-t (fp02 tx x) 
+                          fp39 : Union (* tx) ⊆  (* (SB.i (fp02 tx x)))
+                          fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx x))} (fp40 x txw)
+                          ... | case1 sb = sb
+                          ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw )
+                      fp37 record { owner = owner ; ao = (case2 ax) ; ox = ox } = not (case2 (fp39 record { owner = _ ; ao = ax ; ox = ox }) ) where
+                          fp38 : (L ＼  (* (SB.i (fp02 ty y)))) ⊆ (L ＼ Union (* ty))
+                          fp38 = SB.not-t (fp02 ty y) 
+                          fp39 : Union (* ty) ⊆  (* (SB.i (fp02 ty y)))
+                          fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty y))} (fp40 y tyw)
+                          ... | case1 sb = sb
+                          ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw )
               fp04 :  {tx ty : Ordinal} → & (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) ≡ & (L ＼ * (& (* tx ∪ * ty)))
               fp04 {tx} {ty} = cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
                   fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x