# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719784804 -32400
# Node ID 0b30bb7c75017e4b9844475f5e84208bf964aae1
# Parent  2435deeecda9b216ff27240badaab8f1f9bfd691
...

diff -r 2435deeecda9 -r 0b30bb7c7501 src/BAlgebra.agda
--- a/src/BAlgebra.agda	Sun Jun 30 19:36:51 2024 +0900
+++ b/src/BAlgebra.agda	Mon Jul 01 07:00:04 2024 +0900
@@ -39,6 +39,10 @@
     lem1 : {x : Ordinal} → odef  od∅ x → odef (L ＼ L) x
     lem1 {x} lt = ⊥-elim ( ¬∅∋ (subst (λ k → odef od∅ k) (sym &iso) lt ))
 
+＼-cong : (P Q R S : HOD) → P =h= R → Q =h= S →  (P ＼ Q) =h= (R ＼ S)
+eq→ (＼-cong P Q R S p=r q=s) {x} ⟪ px , npq ⟫ = ⟪ eq→ p=r px , (λ lt → npq (eq← q=s lt) ) ⟫
+eq← (＼-cong P Q R S p=r q=s ) {x} ⟪ rx , nrs ⟫ = ⟪ eq← p=r rx , (λ lt → nrs (eq→ q=s lt) ) ⟫
+
 L＼Lx=x : {x : HOD} →  x ⊆ L   → (L ＼ ( L ＼ x )) =h= x
 L＼Lx=x {x} x⊆L = record { eq→ = lem03 ; eq← = lem04 }  where
     lem03 :  {z : Ordinal} → odef (L ＼ (L ＼ x)) z → odef x z
diff -r 2435deeecda9 -r 0b30bb7c7501 src/Topology.agda
--- a/src/Topology.agda	Sun Jun 30 19:36:51 2024 +0900
+++ b/src/Topology.agda	Mon Jul 01 07:00:04 2024 +0900
@@ -59,6 +59,10 @@
 open import ZProduct O HODAxiom ho<
 open import filter O HODAxiom ho< AC
 
+import Relation.Binary.Reasoning.Setoid as EqHOD
+
+LDec : (L : HOD) (P : HOD) → P ⊆ L → (x : HOD) → Dec (x ∈ P)
+LDec L P _ x = ∋-p P x
 
 record Topology  ( L : HOD ) : Set (suc n) where
    field
@@ -70,26 +74,28 @@
 --- we may add
 --     OS∋L   :  OS ∋ L
 -- closed Set
-   open BAlgebra O HODAxiom ho< L ?
+   open BAlgebra O HODAxiom ho< L (LDec L)
    CS : HOD
    CS = record { od = record { def = λ x → (* x ⊆ L) ∧ odef OS (& ( L ＼ (* x ))) } ; odmax = osuc (& L) ; <odmax = tp02 } where
        tp02 : {y : Ordinal } → (* y ⊆ L) ∧ odef OS (& (L ＼ * y)) → y o< osuc (& L)
        tp02 {y} nop = subst (λ k → k o≤ & L ) &iso ( ⊆→o≤ (λ {x} yx → proj1 nop yx ))
    os⊆L :  {x : HOD} → OS ∋ x → x ⊆ L
-   os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) ? xy  )
+   os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (eq← *iso xy)
    cs⊆L :  {x : HOD} → CS ∋ x → x ⊆ L
-   cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) ? xy )
+   cs⊆L {x} Cx {y} xy = proj1 Cx (eq← *iso xy)
    CS∋L : CS ∋ L
-   CS∋L = ⟪ subst (λ k → k ⊆ L) ? (λ x → x)  , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅  ⟫ where
-        lem0 : L ＼ * (& L) ≡ od∅
-        lem0 = subst (λ k → L ＼ k  ≡ od∅) ? ? -- L＼L=0
+   CS∋L = ⟪ (λ lt → eq→ *iso lt)  , subst (λ k → odef OS k) (sym lem0) OS∋od∅  ⟫ where
+        lem0 : & (L ＼ * (& L)) ≡ & od∅
+        lem0 = ==→o≡ ( ==-trans (＼-cong L (* (& L)) L L ==-refl *iso ) L＼L=0 )
    CS⊆PL :  CS ⊆ Power L
    CS⊆PL {x} Cx y xy = proj1 Cx xy
    P＼CS=OS : {cs : HOD} → CS ∋ cs →  OS ∋ ( L ＼ cs )
-   P＼CS=OS {cs} ⟪ cs⊆L , olcs  ⟫ = subst (λ k → odef OS k) ?  olcs
+   P＼CS=OS {cs} ⟪ cs⊆L , olcs  ⟫ = subst (λ k → odef OS k) (==→o≡ (＼-cong L (* (& cs)) L cs ==-refl *iso))  olcs
    P＼OS=CS : {cs : HOD} → OS ∋ cs →  CS ∋ ( L ＼ cs )
-   P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) ? proj1
-      , subst (λ k → odef OS k) (cong (&) (trans (sym ?) (cong (λ k → L ＼ k) ?) )) oos  ⟫
+   P＼OS=CS {os} oos = ⟪ (λ lt →  proj1 (eq→ *iso lt))
+      , subst (λ k → odef OS k) (==→o≡ (==-sym (==-trans (
+           ＼-cong L (* ( & (L ＼ os)))  L (L ＼ os) ==-refl *iso ) (L＼Lx=x {os} (os⊆L oos)) ))) oos  ⟫
+
 
 open Topology
 
@@ -101,14 +107,15 @@
 
 ClL : {L : HOD} → (top : Topology L) → Cl top L  =h= L
 ClL {L} top  =  record { eq→ = λ {x} ic
-        → subst (λ k → odef k x) ? ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) ? ( λ x → x)))
+        → eq→ *iso ((proj2 ic) (& L) (CS∋L top) (λ lt → eq← *iso lt))
     ; eq← =  λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } 
 
 -- Closure is Closed Set
 
+
 CS∋Cl : {L : HOD} → (top : Topology L) → (A : HOD) → CS top ∋ Cl top A 
-CS∋Cl {L} top A = subst (λ k → CS top ∋ k) ? (P＼OS=CS top UOCl-is-OS)  where
-    open BAlgebra O HODAxiom ho< L ?
+CS∋Cl {L} top A = subst (λ k → odef (CS top)  k) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS)  where
+    open BAlgebra O HODAxiom ho< L (LDec L)
     OCl : HOD  -- set of open set which it not contains A 
     OCl = record { od = record { def = λ o → odef (OS top) o ∧ ( A ⊆ (L ＼ * o) ) } ; odmax = & (OS top) ; <odmax = odef∧< }
     OCl⊆OS  : OCl ⊆  OS top 
@@ -122,28 +129,31 @@
            cc02 : (c : Ordinal) → odef (CS top) c → A ⊆ * c → ¬ odef (Union OCl) x  → odef (* c) x
            cc02 c cc ac nox with ODC.∋-p (* c) (* x)
            ... | yes y = subst (λ k → odef (* c) k) &iso y
-           ... | no ncx = ⊥-elim ( nox record { owner = & ( L ＼ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = subst (λ k → odef k x) ? cc06  } ) where
+           ... | no ncx = ⊥-elim ( nox record { owner = & ( L ＼ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = eq← *iso cc06  } ) where
                 cc06 : odef (L ＼ * c) x 
                 cc06 = ⟪ Lx , subst (λ k → ¬ odef (* c) k) &iso ncx ⟫
                 cc08 : * c ⊆ L
                 cc08 = cs⊆L top (subst (λ k → odef (CS top) k ) (sym &iso) cc )
+                cc09 : (L ＼ * (& (L ＼ * c))) =h= (* c)
+                cc09 = begin 
+                    L ＼ * (& (L ＼ * c)) ≈⟨ ＼-cong L (* (& (L ＼ * c))) L (L ＼ * c) ==-refl *iso  ⟩
+                    L ＼ (L ＼ * c) ≈⟨  L＼Lx=x {* c} cc08 ⟩
+                    * c ∎
+                       where open EqHOD ==-Setoid
                 cc07 :  A ⊆ (L ＼ * (& (L ＼ * c)))
-                cc07 {z} az = subst (λ k → odef k z ) (
-                   begin  * c ≡⟨ sym ? ⟩
-                   L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) ? ⟩
-                   L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning
+                cc07 {z} az = eq← cc09 ( ac az ) 
         cc03 : {x : Ordinal}  → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x) → odef (L ＼ Union OCl) x
         cc03 {x} ⟪ Lx , ccx ⟫ = ⟪ Lx , cc04 ⟫ where
            -- if x is in Cl A, it is in some c : CS, OCl says it is not , i.e. L ＼ o ∋ x, so it is in (L ＼ Union OCl) x
            cc04 : ¬ odef (Union OCl) x
-           cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) ? cc05) ox  where
+           cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( eq→ *iso cc05) ox  where
                 cc05 : odef (* (& (L ＼ * o))) x
-                cc05 = ccx (& (L ＼ * o)) (P＼OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (subst (λ k → A ⊆ k) ? A⊆L-o) 
+                cc05 = ccx (& (L ＼ * o)) (P＼OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (λ lt → eq← *iso (A⊆L-o lt)) 
 
 CS∋x→Clx=x : {L x : HOD} → (top : Topology L) → CS top ∋ x → Cl top x =h= x 
 CS∋x→Clx=x {L} {x} top cx = record { eq→ = cc10 ; eq← = cc11 } where
     cc10 : {y : Ordinal} → odef L y ∧ ((c : Ordinal) → odef (CS top) c → x ⊆ * c → odef (* c) y) → odef x y
-    cc10 {y} ⟪ Ly , cc ⟫ = subst (λ k → odef k y) ? ( cc (& x) cx (λ {z} xz → subst (λ k → odef k z) ? xz  ) )
+    cc10 {y} ⟪ Ly , cc ⟫ = eq→ *iso ( cc (& x) cx (λ {z} xz → eq← *iso xz  ) )
     cc11 : {y : Ordinal} → odef x y → odef L y ∧ ((c : Ordinal) → odef (CS top) c → x ⊆ * c → odef (* c) y) 
     cc11 {y} xy = ⟪ cs⊆L top cx xy , (λ c oc x⊆c → x⊆c xy ) ⟫
 
@@ -163,7 +173,7 @@
 
 is-sbp :  (P : HOD) {x y : Ordinal } → (px : Subbase P x) → odef (* x) y  → odef P (sbp P px ) ∧ odef (* (sbp P px)) y
 is-sbp P {x} (gi px) xy = ⟪ px , xy ⟫
-is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) ?  xy))
+is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (eq→ *iso xy))
 
 sb⊆ : {P Q : HOD} {x : Ordinal } → P ⊆ Q → Subbase P x → Subbase Q x
 sb⊆ {P} {Q} P⊆Q (gi px) = gi (P⊆Q px)
@@ -200,48 +210,48 @@
 InducedTopology L P isb = record { OS = SO L P ; OS⊆PL = tp00
          ; o∪ = tp02 ; o∩ = tp01 ; OS∋od∅ = tp03 } where
     tp03 : {x : Ordinal } → odef (* (& od∅)) x → Base L P (& od∅) x
-    tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j k ) ? (sym &iso) 0x ))
+    tp03 {x} 0x = ⊥-elim ( empty (* x) (eq→ *iso ( subst (λ k → odef (* (& od∅)) k ) (sym &iso) 0x )))
     tp00 : SO L P ⊆ Power L
     tp00 {u} ou x ux  with ou ux
     ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = u⊆L (b⊆u bx)
     tp01 :  {p q : HOD} → SO L P ∋ p → SO L P ∋ q → SO L P ∋ (p ∩ q)
-    tp01 {p} {q} op oq {x} ux =  record { b = b ; u⊆L = subst (λ k → k ⊆ L) ? ul
+    tp01 {p} {q} op oq {x} ux =  record { b = b ; u⊆L = λ lt → ul (eq→ *iso lt)
       ; sb = g∩ (Base.sb (op px)) (Base.sb (oq qx))   ; b⊆u = tp08 ; bx = tp14 } where
         px : odef (* (& p)) x
-        px = subst (λ k → odef k x ) ? ( proj1 (subst (λ k → odef k _ ) ? ux ) )
+        px = eq← *iso ( proj1 (eq→ *iso ux) )
         qx : odef (* (& q)) x
-        qx = subst (λ k → odef k x ) ? ( proj2 (subst (λ k → odef k _ ) ? ux ) )
+        qx = eq← *iso ( proj2 (eq→ *iso ux) )
         b : Ordinal
         b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx)))
         tp08 :  * b ⊆ * (& (p ∩ q) )
-        tp08 =  subst₂ (λ j k → j ⊆ k ) ?  ? (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where
+        tp08 = λ lt → ( eq← *iso ((⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) (eq→ *iso lt))) where
              tp11 : * (Base.b (op px))  ⊆ * (& p )
              tp11 = Base.b⊆u (op px)
              tp12 : * (Base.b (oq qx))  ⊆ * (& q )
              tp12 = Base.b⊆u (oq qx)
              tp09 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ p
-             tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) ? tp11)
+             tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (λ lt → eq→ *iso (tp11 lt))
              tp10 : (* (Base.b (op px)) ∩ * (Base.b (oq qx))) ⊆ q
-             tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) ? tp12)
+             tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (λ lt → eq→ *iso (tp12 lt))
         tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x
-        tp14 = subst (λ k → odef k x ) ? ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫
+        tp14 = eq← *iso ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫
         ul :  (p ∩ q) ⊆ L
-        ul = subst (λ k → k ⊆ L ) ? (λ {z} pq →  (Base.u⊆L (op px)) (pz pq) )  where
+        ul = λ pq →  (Base.u⊆L (op px)) (pz (eq← *iso pq)) where
             pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z
-            pz {z} pq = subst (λ k → odef k z ) ? ( proj1 (subst (λ k → odef k _ ) ? pq ) )
+            pz {z} pq = eq← *iso ( proj1 (eq→ *iso pq ) )
     tp02 : { q : HOD} → q ⊆ SO L P → SO L P ∋ Union q
-    tp02 {q} q⊆O {x} = ? -- ux with subst (λ k → odef k x) ? ux
-    -- . | record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx
-    -- . | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊆L = subst (λ k → k ⊆ L) ? tp04
-    --      ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) ? tp06  ; bx = bx } where
-    --   tp05 :  Union q ⊆ L
-    --   tp05 {z} record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx
-    --   ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx }
-    --      = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx ))
-    --   tp04 :  Union q ⊆ L
-    --   tp04 = tp05
-    --   tp06 : * b ⊆ Union q
-    --   tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz  }
+    tp02 {q} q⊆O {x} ux with eq→ *iso ux
+    ... | record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx
+    ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx } = record { b = b ; u⊆L = λ lt → tp04 (eq→ *iso lt)
+         ; sb = sb ; b⊆u = λ lt → eq← *iso (tp06 lt)  ; bx = bx } where
+      tp05 :  Union q ⊆ L
+      tp05 {z} record { owner = y ; ao = qy ; ox = yx } with q⊆O qy yx
+      ... | record { b = b ; u⊆L = u⊆L ; sb = sb ; b⊆u = b⊆u ; bx = bx }
+         = IsSubBase.P⊆PL isb (proj1 (is-sbp P sb bx )) _ (proj2 (is-sbp P sb bx )) 
+      tp04 :  Union q ⊆ L
+      tp04 = tp05
+      tp06 : * b ⊆ Union q
+      tp06 {z} bz = record { owner = y ; ao = qy ; ox = b⊆u bz  }
 
 -- Product Topology
 
@@ -341,7 +351,7 @@
    fip00 {X} xo xcp = fin-e 
 ... | tri> ¬a ¬b 0<L = record { finCover = finCover ; isCover = isCover1 ; isFinite = isFinite } where
    -- set of coset of X
-   open BAlgebra O HODAxiom ho< L  ?
+   open BAlgebra O HODAxiom ho< L  (LDec L)
    CX : {X : Ordinal} → * X ⊆ OS top → Ordinal
    CX {X} ox = & ( Replace (* X) (λ z → L ＼  z ) RC＼ )
    CCX : {X : Ordinal} → (os :  * X ⊆ OS top) → * (CX os) ⊆ CS top
@@ -481,7 +491,7 @@
    ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 ... | tri> ¬a ¬b 0<L = record { limit = limit ; is-limit = fip00 } where
    -- set of coset of X
-   open BAlgebra O HODAxiom ho< L ?
+   open BAlgebra O HODAxiom ho< L (LDec L)
    OX : {X : Ordinal} → * X ⊆ CS top → Ordinal
    OX {X} ox = & ( Replace (* X) (λ z → L ＼  z ) RC＼)
    OOX : {X : Ordinal} → (cs :  * X ⊆ CS top) → * (OX cs) ⊆ OS top
@@ -691,9 +701,14 @@
 
 CAP : (P : HOD) {p q : HOD } → Power P ∋ p → Power P ∋ q → Power P ∋ (p ∩ q)
 CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) ? pqx
-... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) ? px )
+... | t = ?
+-- ... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) ? px )
 
 NEG : (P : HOD) {p : HOD } → Power P ∋ p → Power P ∋ (P ＼ p )
 NEG P {p} Pp x vx with subst (λ k → odef k x) ? vx
-... | ⟪ Px , npx ⟫ = Px
+... | t = ?
+-- ... | ⟪ Px , npx ⟫ = Px
 
+
+
+