# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719819432 -32400
# Node ID 1925debf28bb86c9631eced3ec46e42cbe85ef36
# Parent  49c3ef1e9b4f22b9e26c94b915324471cdbc86c5
Tychonoff start

diff -r 49c3ef1e9b4f -r 1925debf28bb src/Tychonoff.agda
--- a/src/Tychonoff.agda	Mon Jul 01 16:07:57 2024 +0900
+++ b/src/Tychonoff.agda	Mon Jul 01 16:37:12 2024 +0900
@@ -1,40 +1,66 @@
-{-# OPTIONS --allow-unsolved-metas #-}
+{-# OPTIONS --cubical-compatible --safe #-}
+open import Level
+open import Ordinals
+open import logic
+open import Relation.Nullary
+
 open import Level
 open import Ordinals
-module Tychonoff {n : Level } (O : Ordinals {n})   where
+import HODBase
+import OD
+open import Relation.Nullary
+module Tychonoff {n : Level } (O : Ordinals {n})   (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom )
+       (AC : OD.AxiomOfChoice O HODAxiom ) where
+
+
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Binary.Definitions
+
+open import Data.Empty
+
+import OrdUtil
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+import ODUtil
 
 open import logic
+open import nat
+
+open OrdUtil O
+open ODUtil O HODAxiom  ho<
+
 open _∧_
 open _∨_
 open Bool
 
-import OD
-open import Relation.Nullary
-open import Data.Empty
-open import Relation.Binary.Core
-open import Relation.Binary.Definitions
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+open AxiomOfChoice AC
+open import ODC O HODAxiom AC as ODC
+
+open import Level
+open import Ordinals
+
+open import Relation.Nullary 
+-- open import Relation.Binary hiding ( _⇔_ )
+open import Data.Empty 
 open import Relation.Binary.PropositionalEquality
-import BAlgebra
-open BAlgebra O
-open inOrdinal O
-open OD O
-open OD.OD
-open ODAxiom odAxiom
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
--- open Ordinals.IsNext isNext
-open OrdUtil O
-open ODUtil O
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+import BAlgebra 
 
-import ODC
-open ODC O
+open import ZProduct O HODAxiom ho<
+open import filter O HODAxiom ho< AC
+open import filter-util O HODAxiom ho< AC
 
-open import filter O
-open import filter-util O
-open import ZProduct O
-open import Topology O
+import Relation.Binary.Reasoning.Setoid as EqHOD
+
+open import Topology O HODAxiom ho< AC
 
 open Filter
 open Topology
@@ -108,17 +134,17 @@
    --   if 0 < X then 0 < x ∧ P ∋ xfrom fip
    --   if 0 ≡ X then ¬ odef X x
    fip03 {X} CX fip {x} xx with trio< o∅ X
-   ... | tri< 0<X ¬b ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso)
-        ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx))  xe ))) where
+   ... | tri< 0<X ¬b ¬c = ? where -- ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) P=0)) o∅≡od∅ ) (sym &iso)
+        -- ( cs⊆L TP (subst (λ k → odef (CS TP) k ) (sym &iso) (CX xx))  xe ))) where
       0<x : o∅ o< x
       0<x = fip (gi xx )
       e : HOD  -- we have an element of x
-      e = ODC.minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
+      e = minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
       xe : odef (* x) (& e)
-      xe = ODC.x∋minimal O (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
+      xe = x∋minimal (* x) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<x) )
    ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ( begin
            * X ≡⟨ cong (*) (sym 0=X) ⟩
-           * o∅ ≡⟨  o∅≡od∅ ⟩
+           * o∅ ≡⟨ ? ⟩ --  o∅≡od∅ ⟩
            od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
    ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 ... | tri> ¬a ¬b 0<P = record { limit = λ CSX fip → limit CSX fip ; is-limit =  uf01 } where
@@ -131,22 +157,22 @@
      N⊆PP CSX fp nx b xb  = FBase.u⊆P nx xb
      -- filter base is not empty,  it is necessary to maximize fip filter 
      nc : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fip : fip CSX) → HOD
-     nc {X} 0<X CSX fip = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X
+     nc {X} 0<X CSX fip = minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) ) -- an element of X
      N∋nc :{X : Ordinal} → (0<X : o∅ o< X) → (CSX : * X ⊆ CS TP)
         → (fip : fip CSX) → odef (N CSX fip) (& (nc 0<X CSX fip) )
      N∋nc {X} 0<X CSX fip = record { b = X ; x =  & e ;  b⊆X = λ x → x ; sb = gi Xe ; u⊆P = nn02 ; x⊆u = λ x → x } where
           e : HOD  -- we have an element of X
-          e = ODC.minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
+          e = minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
           Xe : odef (* X) (& e)
-          Xe = ODC.x∋minimal O (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
-          nn01 = ODC.minimal O (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) )
+          Xe = x∋minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
+          nn01 = minimal (* (& e)) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) (fip (gi Xe))) )
           nn02 : * (& (nc 0<X CSX fip)) ⊆ P
-          nn02 = subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) )
+          nn02 = ? -- subst (λ k → k ⊆ P ) (sym *iso) (cs⊆L TP (CSX Xe ) )
 
      0<PP : o∅ o< & (Power P)     -- Power P contaisn od∅, so it is not empty
      0<PP = subst (λ k → k o< & (Power P)) &iso ( c<→o< (subst (λ k → odef (Power P) k) (sym &iso) nn00 )) where
           nn00 : odef (Power P) o∅
-          nn00 x lt with subst (λ k → odef k x) o∅≡od∅ lt
+          nn00 x lt with subst (λ k → odef k x) ? lt -- o∅≡od∅ lt
           ... | x<0 = ⊥-elim ( ¬x<0 x<0)
      --
      -- FIP defines a filter
@@ -155,32 +181,33 @@
      F {X} CSX fp = record { filter = N CSX fp ; f⊆L = N⊆PP CSX fp ; filter1 = f1 ; filter2 = f2 } where
          f1 :  {p q : HOD} → Power P ∋ q → N CSX fp ∋ p → p ⊆ q → N CSX fp ∋ q
          f1 {p} {q} Xq record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = Xp ; x⊆u = x⊆p } p⊆q =
-                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = subst (λ k → k ⊆ P) (sym *iso) f10 ; x⊆u = λ {z} xp →
-                            subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } where
+                       record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = ? -- subst (λ k → k ⊆ P) (sym *iso) f10 
+                          ; x⊆u = λ {z} xp → ? } where
+                            -- subst (λ k → odef k z) (sym *iso) (p⊆q (subst (λ k → odef k z) *iso (x⊆p xp)))  } where
               f10 : q ⊆ P
               f10 {x} qx = subst (λ k → odef P k) &iso (power→ P _ Xq (subst (λ k → odef q k) (sym &iso) qx  ))
          f2 : {p q : HOD} → N CSX fp ∋ p → N CSX fp ∋ q → Power P ∋ (p ∩ q) → N CSX fp ∋ (p ∩ q)
          f2 {p} {q} Np Nq Xpq = record { b = & Np+Nq ; x = & xp∧xq ; b⊆X = f20 ; sb = sbpq ; u⊆P = p∩q⊆p ; x⊆u = f22 } where
               p∩q⊆p : * (& (p ∩ q)) ⊆ P
-              p∩q⊆p {x} pqx = subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
+              p∩q⊆p {x} pqx = ? -- subst (λ k → odef P k) &iso (power→ P _ Xpq (subst₂ (λ j k → odef j k ) *iso (sym &iso) pqx ))
               Np+Nq = * (FBase.b Np) ∪ * (FBase.b Nq)
               xp∧xq = * (FBase.x Np) ∩ * (FBase.x Nq)
               sbpq : Subbase (* (& Np+Nq)) (& xp∧xq)
-              sbpq = subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
+              sbpq = ? -- subst₂ (λ j k → Subbase j k ) (sym *iso) refl (  g∩ (sb⊆ case1 (FBase.sb Np)) (sb⊆ case2 (FBase.sb Nq)))
               f20 : * (& Np+Nq) ⊆ * X
-              f20 {x} npq with subst (λ k → odef k x) *iso npq
+              f20 {x} npq with eq→ *iso npq
               ... | case1 np = FBase.b⊆X Np np
               ... | case2 nq = FBase.b⊆X Nq nq
               f22 : * (& xp∧xq) ⊆ * (& (p ∩ q))
-              f22 = subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
-                 → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
+              f22 = ? -- subst₂ ( λ j k → j ⊆ k ) (sym *iso) (sym *iso) (λ {w} xpq
+                 -- → ⟪ subst (λ k → odef k w) *iso ( FBase.x⊆u Np (proj1 xpq)) ,  subst (λ k → odef k w) *iso ( FBase.x⊆u Nq (proj2 xpq)) ⟫ )
      --
      -- it contains no empty sets becase it is a finite intersection ( Subbase (* X) x )
      --
      proper : {X : Ordinal} → (CSX : * X ⊆ CS TP) → (fip : fip {X} CSX) → ¬ (N CSX fip ∋ od∅)
      proper {X} CSX fip record { b = b ; x = x ; b⊆X = b⊆X ; sb = sb ; u⊆P = u⊆P ; x⊆u = x⊆u } = o≤> x≤0 (fip (fp00 _ _ b⊆X sb)) where
           x≤0 : x o< osuc  o∅
-          x≤0 = subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u))
+          x≤0 = ? -- subst₂ (λ j k → j o< osuc k) &iso (trans (cong (&) *iso) ord-od∅ ) (⊆→o≤ (x⊆u))
           fp00 : (b x : Ordinal) → * b ⊆ * X → Subbase (* b) x → Subbase (* X) x
           fp00 b y b<X (gi by ) = gi ( b<X by )
           fp00 b _ b<X (g∩ {y} {z} sy sz ) = g∩ (fp00 _ _ b<X sy) (fp00 _ _ b<X sz)
@@ -198,6 +225,7 @@
      -- ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
      -- ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
 
+     
      postulate 
         maxf   : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
      mf     : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
@@ -215,12 +243,14 @@
      --
      -- the limit is an limit of entire elements of X
      --
+     open BAlgebra O HODAxiom ho< P (LDec P)
+
      uf01 :  {X : Ordinal} (CSX : * X ⊆ CS TP) (fp : fip {X} CSX) {x : Ordinal} → odef (* X) x → odef (* x) (limit CSX fp)
      uf01 {X} CSX fp {x} xx with trio< o∅ X
      ... | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
      ... | tri≈ ¬a 0=X ¬c = ⊥-elim ( ¬a (subst (λ k → o∅ o< k) &iso ( ∈∅< xx )))
      --  0<X  limit is in * x or P ＼ * x
-     ... | tri< 0<X ¬b ¬c with ∨L＼X {P} {* x} {UFLP.limit ( uflp  ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))}
+     ... | tri< 0<X ¬b ¬c with ∨L＼X {* x} {UFLP.limit ( uflp  ( mf 0<X CSX fp ) (ultraf 0<X CSX fp))}
          (UFLP.P∋limit ( uflp  ( mf 0<X CSX fp ) (ultraf 0<X CSX fp)))
      ... | case1 lt = lt -- odef (* x) y
      ... | case2 nlxy = ⊥-elim (MaximumFilter.proper (maxf 0<X CSX fp) uf11 ) where
@@ -235,16 +265,17 @@
         uf10 = nlxy
         uf03 : Neighbor TP y (& (P ＼ * x ))
         uf03 = record { u = _ ; ou = P＼CS=OS TP (CSX (subst (λ k → odef (* X) k ) (sym &iso) xx))
-           ; ux = subst (λ k → odef k y) (sym *iso) uf10
-           ; v⊆P = λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz )
+           ; ux = ? -- subst (λ k → odef k y) (sym *iso) uf10
+           ; v⊆P = ? -- λ {z} xz → proj1 (subst(λ k → odef k z) *iso xz )
            ; u⊆v = λ x → x  }
         uf07 : * (& (* x , * x)) ⊆ * X
-        uf07 {y} lt with subst (λ k → odef k y) *iso lt
+        uf07 {y} lt with eq→ *iso lt
         ... | case1 refl = subst (λ k → odef (* X) k ) (sym &iso) xx
         ... | case2 refl = subst (λ k → odef (* X) k ) (sym &iso) xx
         uf05 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) x
         uf05 = MaximumFilter.F⊆mf (maxf 0<X CSX fp) record { b = & (* x , * x) ; b⊆X = uf07
-           ; sb = gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) )  ; u⊆P = x⊆P ; x⊆u = λ x → x  }
+           ; sb = ? --- gi (subst (λ k → odef k x) (sym *iso) (case1 (sym &iso)) )  
+           ; u⊆P = x⊆P ; x⊆u = λ x → x  }
         -- if we postulate maximum filter, uf061 is an error
         -- uf061 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (* (& (P ＼ * x ))))
         -- uf061 = UFLP.is-limit ( uflp (mf 0<X CSX fp) (ultraf 0<X CSX fp)) {& (P ＼ * x)} uf03
@@ -254,11 +285,11 @@
         uf06 : odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) (& (P ＼ * x ))
         uf06 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k) &iso uf063
         uf13 : & ((* x) ∩ (P ＼ * x )) ≡ o∅
-        uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) }  ) ) where
+        uf13 = subst₂ (λ j k → j ≡ k ) refl ord-od∅ (cong (&) ? ) where -- ( ==→o≡ record { eq→ = uf14 ; eq← = λ {x} lt → ⊥-elim (¬x<0 lt) }  ) ) where
            uf14 : {y : Ordinal} → odef (* x ∩ (P ＼ * x)) y → odef od∅ y
            uf14 {y} ⟪ xy , ⟪ Px , ¬xy ⟫ ⟫ = ⊥-elim ( ¬xy xy )
         uf12 : odef (Power P) (& ((* x) ∩ (P ＼ * x )))
-        uf12 z pz with subst (λ k → odef k z) *iso pz
+        uf12 z pz with eq→ *iso pz
         ... | ⟪ xz , ⟪ Pz , ¬xz ⟫ ⟫ = Pz
         uf11 : filter (MaximumFilter.mf (maxf 0<X CSX fp)) ∋ od∅
         uf11 = subst (λ k → odef (filter (MaximumFilter.mf (maxf 0<X CSX fp))) k ) (trans uf13 (sym ord-od∅))
@@ -278,12 +309,12 @@
 --
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
-FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
+FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01
    ; P∋limit = ufl10 ; is-limit = ufl00 } where
      F∋P : odef (filter F) (& P)
-     F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) )  (λ z az → proj1 (subst (λ k → odef k z) *iso az ) )
+     F∋P with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (eq→ *iso az)) )  (λ z az → proj1 (eq→ *iso az ) )
      ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp )
-     ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20))  flp where
+     ... | case2 flp = subst (λ k → odef (filter F) k) (==→o≡ fl20)  flp where
          fl20 :  (P ＼ Ord o∅) =h=  P
          fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) )  ⟫  }
      0<P : o∅ o< & P
@@ -302,10 +333,10 @@
      -- it is set of closed set and has FIP ( F is proper )
      --
      ufl08  : {z : Ordinal} → odef (Power P) (& (Cl TP (* z)))
-     ufl08 {z} w zw with subst (λ k → odef k w ) *iso zw
+     ufl08 {z} w zw with eq→ *iso zw
      ... | t = proj1 t
      fx→px : {x : Ordinal} → odef (filter F) x → Power P ∋ * x
-     fx→px {x} fx z xz = f⊆L F fx _ (subst (λ k → odef k z) *iso xz )
+     fx→px {x} fx z xz = f⊆L F fx _ (eq→ *iso xz )
      F∋sb : {x : Ordinal} → Subbase CF x → odef (filter F) x
      F∋sb {x} (gi record { z = z ; az = az ; x=ψz = x=ψz }) = ufl07 where
         ufl09 : * z ⊆ P
@@ -313,10 +344,11 @@
         ufl07 : odef (filter F) x
         ufl07 = subst (λ k → odef (filter F) k) &iso ( filter1 F (subst (λ k → odef (Power P) k) (trans (sym x=ψz) (sym &iso))  ufl08  )
             (subst (λ k → odef (filter F) k) (sym &iso) az)
-            (subst (λ k → * z ⊆ k ) (trans (sym *iso) (sym (cong (*) x=ψz)) ) (x⊆Clx TP {* z} ufl09 ) ))
+            (subst (λ k → * z ⊆ k ) ? -- (trans (sym *iso) (sym (cong (*) x=ψz)) ) 
+               (x⊆Clx TP {* z} ufl09 ) ))
      F∋sb  (g∩ {x} {y} sx sy) = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sx))
         (subst (λ k → odef (filter F) k) (sym &iso) (F∋sb sy))
-            (λ z xz → fx→px (F∋sb sx) _ (subst (λ k → odef k _) (sym *iso) (proj1 (subst (λ k → odef k z) *iso xz) )))
+            (λ z xz → fx→px (F∋sb sx) _ (eq← *iso (proj1 (eq→ *iso xz) )))
      ufl01 : {x : Ordinal} → Subbase (* (& CF)) x → o∅ o< x
      ufl01 {x} sb = ufl04  where
         ufl04 : o∅ o< x
@@ -326,19 +358,21 @@
            begin
            x  ≡⟨ sym b ⟩
            o∅ ≡⟨ sym ord-od∅ ⟩
-           & od∅  ∎ ) (F∋sb (subst (λ k → Subbase k x) *iso sb )) ))  where open ≡-Reasoning
+           & od∅  ∎ ) ? -- (F∋sb (subst (λ k → Subbase k x) *iso sb ))
+              ))  where open ≡-Reasoning
         ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
-     ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01)
-     ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01 {& P} ufl11  where
+     ufl10 : odef P (FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01)
+     ufl10 = FIP.L∋limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01 {& P} ufl11  where
          ufl11 : odef (* (& CF)) (& P)
-         ufl11 = subst (λ k → odef k (& P)) (sym *iso) record { z = _ ; az  = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) *iso) (ClL TP)))   }
+         ufl11 = eq← *iso record { z = _ ; az  = F∋P ; x=ψz = sym (cong (&) (trans (cong (Cl TP) ? ) ? -- (ClL TP)
+            ))   }
      --
      -- so we have a limit
      --
      limit : Ordinal
-     limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
+     limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01
      ufl02 : {y : Ordinal } → odef (* (& CF)) y → odef (* y) limit
-     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
+     ufl02 = FIP.is-limit fip (subst (λ k → k ⊆ CS TP) ? CF⊆CS) ufl01
      --
      -- Neigbor of limit ⊆ Filter
      --
@@ -350,23 +384,23 @@
      --      this contradicts ufl02
      pp :  {v : Ordinal} → (nei : Neighbor TP limit v ) → Power P ∋ (* (Neighbor.u nei))
      pp {v} record { u = u ; ou = ou ; ux = ux ; v⊆P = v⊆P ; u⊆v = u⊆v } z pz
-        = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (subst (λ k → odef k z) *iso pz )
+        = os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) ou ) (eq→ *iso pz )
      ufl00 :  {v : Ordinal} → Neighbor TP limit v → filter F ∋ * v
      ufl00 {v} nei with ultra-filter.ultra UF (pp nei ) (NEG P (pp nei ))
      ... | case1 fu = subst (λ k → odef (filter F) k) &iso
-       ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px)  fu (subst (λ k → u ⊆ k ) (sym *iso) (Neighbor.u⊆v nei))) where
+       ( filter1 F (subst (λ k → odef (Power P) k ) (sym &iso) px)  fu (subst (λ k → u ⊆ k ) ? (Neighbor.u⊆v nei))) where
          u = * (Neighbor.u nei)
          px : Power P ∋ * v
-         px z vz = Neighbor.v⊆P nei (subst (λ k → odef k z) *iso vz )
+         px z vz = Neighbor.v⊆P nei (eq→ *iso vz )
      ... | case2 nfu = ⊥-elim ( ¬P\u∋limit P\u∋limit ) where
          u = * (Neighbor.u nei)
          P\u : HOD
          P\u = P ＼ u
          P\u∋limit : odef P\u limit
-         P\u∋limit = subst (λ k → odef k limit) *iso ( ufl02 (subst (λ k → odef k (& P\u)) (sym *iso) ufl03 )) where
+         P\u∋limit = eq→ *iso ( ufl02 (subst (λ k → odef k (& P\u)) ? ufl03 )) where
              ufl04 : & P\u ≡ & (Cl TP (* (& P\u)))
-             ufl04 = cong (&) (sym (trans (cong (Cl TP) *iso)
-                (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) )))))
+             ufl04 = cong (&) (sym (trans (cong (Cl TP) ? ) ? ))
+                -- (CS∋x→Clx=x TP (P＼OS=CS TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou nei) )))))
              ufl03 : odef CF (& P\u )
              ufl03 = record { z = _ ; az = nfu ; x=ψz = ufl04 }
          ¬P\u∋limit : ¬ odef P\u limit
@@ -397,9 +431,9 @@
              → UFLP (ProductTopology TP TQ) F UF
      uflPQ F UF = record { limit = & < * ( UFLP.limit uflp ) , * ( UFLP.limit uflq ) >  ; P∋limit = Pf ; is-limit = isL } where
          F∋PQ : odef (filter F) (& (ZFP P Q))
-         F∋PQ with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (subst (λ k → odef k z) *iso az)) )  (λ z az → proj1 (subst (λ k → odef k z) *iso az ) )
+         F∋PQ with ultra-filter.ultra UF {od∅} (λ z az → ⊥-elim (¬x<0 (eq→ *iso az)) )  (λ z az → proj1 (eq→ *iso az ) )
          ... | case1 fp = ⊥-elim ( ultra-filter.proper UF fp )
-         ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20))  flp where
+         ... | case2 flp = subst (λ k → odef (filter F) k) (==→o≡ fl20)  flp where
              fl20 :  (ZFP P Q ＼ Ord o∅) =h=  ZFP P Q
              fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) )  ⟫  }
          0<PQ : o∅ o< & (ZFP P Q)
@@ -408,15 +442,15 @@
          ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋PQ) )
          ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
          apq : HOD
-         apq = ODC.minimal O (ZFP P Q) (0<P→ne 0<PQ)
+         apq = minimal (ZFP P Q) (0<P→ne 0<PQ)
          is-apq : ZFP P Q ∋ apq
-         is-apq = ODC.x∋minimal O (ZFP P Q) (0<P→ne 0<PQ)
+         is-apq = x∋minimal (ZFP P Q) (0<P→ne 0<PQ)
          ap : odef P ( zπ1 is-apq  )
          ap = zp1 is-apq
          aq : odef Q ( zπ2 is-apq  )
          aq = zp2 is-apq
          F⊆pxq : {x : HOD } → filter F ∋ x →  x ⊆ ZFP P Q
-         F⊆pxq {x} fx {y} xy = f⊆L F fx y (subst (λ k → odef k y) (sym *iso) xy)
+         F⊆pxq {x} fx {y} xy = f⊆L F fx y (eq← *iso xy)
 
          ---
          --- FP is a P-projection of F, which is a ultra filter
@@ -448,7 +482,7 @@
          Pf = ab-pair (UFLP.P∋limit uflp) (UFLP.P∋limit uflq)
 
          isL : {v : Ordinal} → Neighbor (ProductTopology TP TQ) (& < * (UFLP.limit uflp) , * (UFLP.limit uflq) >) v → filter F ∋ * v
-         isL {v} nei = filter1 F (λ z xz → Neighbor.v⊆P nei (subst (λ k → odef k z) *iso xz))
+         isL {v} nei = filter1 F (λ z xz → Neighbor.v⊆P nei (eq→ *iso xz))
                 (subst (λ k → odef (filter F) k) (sym &iso) (F∋base pqb b∋l )) bpq⊆v where
              --
              -- Product Topolgy's open set contains a subbase which is an element of ZPF p Q or ZPF P q
@@ -473,13 +507,13 @@
                  --  subbase of product topology which includes lim is in FP, so in F
                  --
                  isl00 : odef (ZFP (* (BaseP.p px)) Q) lim
-                 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseP.prod px)) *iso )  bl
+                 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseP.prod px)) ? )  bl
                  px∋limit : odef (* (BaseP.p px)) (UFLP.limit uflp)
                  px∋limit = isl01 isl00 refl where
                     isl01 : {x : Ordinal } → odef (ZFP (* (BaseP.p px)) Q) x → x ≡ lim →  odef (* (BaseP.p px)) (UFLP.limit uflp)
                     isl01 (ab-pair {a} {b} bx qx) ab=lim = subst (λ k → odef (* (BaseP.p px)) k) a=lim bx where
                        a=lim : a ≡ UFLP.limit uflp
-                       a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) )))
+                       a=lim = subst₂ (λ j k → j ≡ k ) &iso &iso ? -- (cong (&) (proj1 ( prod-≡ (subst₂ (λ j k → j ≡ k ) ? ? (cong (*) ab=lim) ) )))
                  fp∋b : filter FP ∋ * (BaseP.p px)
                  fp∋b = UFLP.is-limit uflp record { u = _ ; ou = BaseP.op px ; ux = px∋limit
                      ; v⊆P = λ {x} lt → os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) (BaseP.op px)) lt ; u⊆v = λ x → x }
@@ -487,13 +521,13 @@
                  f∋b = FPSet⊆F1 (subst (λ k → odef (filter FP) k ) &iso fp∋b )
              F∋base {b} (gi (case2 qx)) bl  = subst (λ k → odef (filter F) k) (sym (BaseQ.prod qx)) f∋b where
                  isl00 : odef (ZFP P (* (BaseQ.q qx))) lim
-                 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseQ.prod qx)) *iso )  bl
+                 isl00 = subst (λ k → odef k lim ) (trans (cong (*) (BaseQ.prod qx)) ? )  bl
                  qx∋limit : odef (* (BaseQ.q qx)) (UFLP.limit uflq)
                  qx∋limit = isl01 isl00 refl where
                     isl01 : {x : Ordinal } → odef (ZFP P (* (BaseQ.q qx)) ) x → x ≡ lim →  odef (* (BaseQ.q qx)) (UFLP.limit uflq)
                     isl01 (ab-pair {a} {b} px bx) ab=lim = subst (λ k → odef (* (BaseQ.q qx)) k) b=lim bx where
                        b=lim : b ≡ UFLP.limit uflq
-                       b=lim = subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) )))
+                       b=lim = ? -- subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 ( prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ab=lim) ) )))
                  fp∋b : filter FQ ∋ * (BaseQ.q qx)
                  fp∋b = UFLP.is-limit uflq record { u = _ ; ou = BaseQ.oq qx ; ux = qx∋limit
                      ; v⊆P = λ {x} lt → os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) (BaseQ.oq qx)) lt ; u⊆v = λ x → x }
@@ -502,9 +536,9 @@
              F∋base (g∩ {x} {y} b1 b2) bl = F∋x∩y where
                  -- filter contains finite intersection
                  fb01 :  odef (filter F) x
-                 fb01 = F∋base b1 (proj1 (subst (λ k → odef k lim) *iso bl))
+                 fb01 = F∋base b1 (proj1 (eq→ *iso bl))
                  fb02 :  odef (filter F) y
-                 fb02 = F∋base b2 (proj2 (subst (λ k → odef k lim) *iso bl))
+                 fb02 = F∋base b2 (proj2 (eq→ *iso bl))
                  F∋x∩y : odef (filter F) (& (* x ∩ * y))
                  F∋x∩y = filter2 F (subst (λ k → odef (filter F) k) (sym &iso) fb01) (subst (λ k → odef (filter F) k) (sym &iso) fb02)
                     (CAP (ZFP P Q) (subst (λ k → odef (Power (ZFP P Q)) k) (sym &iso) (f⊆L F fb01))