# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1719575738 -32400
# Node ID 32001d93755b155b31437673f2bb09f1fe9caeff
# Parent  6752e2ff4dc640299ea6d88948e23098dce11810
...

diff -r 6752e2ff4dc6 -r 32001d93755b src/Topology.agda
--- a/src/Topology.agda	Fri Jun 28 17:41:43 2024 +0900
+++ b/src/Topology.agda	Fri Jun 28 20:55:38 2024 +0900
@@ -1,39 +1,64 @@
-{-# 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 Topology {n : Level } (O : Ordinals {n})   where
+import HODBase
+import OD
+open import Relation.Nullary
+module Topology {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
+
+import filter 
+
+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 O
-open import ZProduct O
 
 record Topology  ( L : HOD ) : Set (suc n) where
    field
@@ -45,25 +70,26 @@
 --- we may add
 --     OS∋L   :  OS ∋ L
 -- closed Set
+   open BAlgebra O HODAxiom ho< 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) (sym *iso) xy  )
+   os⊆L {x} Ox {y} xy = ( OS⊆PL Ox ) _ (subst (λ k → odef k y) ? xy  )
    cs⊆L :  {x : HOD} → CS ∋ x → x ⊆ L
-   cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) (sym *iso) xy )
+   cs⊆L {x} Cx {y} xy = proj1 Cx (subst (λ k → odef k y ) ? xy )
    CS∋L : CS ∋ L
-   CS∋L = ⟪ subst (λ k → k ⊆ L) (sym *iso) (λ x → x)  , subst (λ k → odef OS (& k)) (sym lem0) OS∋od∅  ⟫ where
+   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∅) (sym *iso) L＼L=0
+        lem0 = subst (λ k → L ＼ k  ≡ od∅) ? ? -- 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) (cong (λ k → & ( L ＼ k)) *iso)  olcs
+   P＼CS=OS {cs} ⟪ cs⊆L , olcs  ⟫ = subst (λ k → odef OS k) ?  olcs
    P＼OS=CS : {cs : HOD} → OS ∋ cs →  CS ∋ ( L ＼ cs )
-   P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) (sym *iso) proj1
-      , subst (λ k → odef OS k) (cong (&) (trans (sym (L＼Lx=x (os⊆L oos))) (cong (λ k → L ＼ k) (sym *iso)) )) oos  ⟫
+   P＼OS=CS {os} oos = ⟪ subst (λ k → k ⊆ L) ? proj1
+      , subst (λ k → odef OS k) (cong (&) (trans (sym ?) (cong (λ k → L ＼ k) ?) )) oos  ⟫
 
 open Topology
 
@@ -73,15 +99,16 @@
 Cl {L} top A = record { od = record { def = λ x → odef L x ∧ ( (c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x ) }
   ; odmax = & L ; <odmax = odef∧< }
 
-ClL : {L : HOD} → (top : Topology L) → Cl top L  ≡ L
-ClL {L} top  =  ==→o≡ ( record { eq→ = λ {x} ic
-        → subst (λ k → odef k x) *iso ((proj2 ic) (& L) (CS∋L top) (subst (λ k → L ⊆ k) (sym *iso) ( λ x → x)))
-    ; eq← =  λ {x} lx → ⟪ lx , ( λ c cs l⊆c → l⊆c lx) ⟫ } )
+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← =  λ {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) (==→o≡ cc00) (P＼OS=CS top UOCl-is-OS)  where
+CS∋Cl {L} top A = subst (λ k → CS top ∋ k) ? (P＼OS=CS top UOCl-is-OS)  where
+    open BAlgebra O HODAxiom ho< 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 
@@ -93,30 +120,30 @@
         cc01 : {x : Ordinal} → odef (L ＼ Union OCl) x → odef L x ∧ ((c : Ordinal) → odef (CS top) c → A ⊆ * c → odef (* c) x)
         cc01 {x} ⟪ Lx , nul ⟫ = ⟪ Lx , ( λ c cc ac → cc02 c cc ac nul ) ⟫ where 
            cc02 : (c : Ordinal) → odef (CS top) c → A ⊆ * c → ¬ odef (Union OCl) x  → odef (* c) x
-           cc02 c cc ac nox with ODC.∋-p O (* 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) (sym *iso) cc06  } ) where
+           ... | no ncx = ⊥-elim ( nox record { owner = & ( L ＼ * c) ; ao = ⟪ proj2 cc , cc07 ⟫ ; ox = subst (λ k → odef k x) ? 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 )
                 cc07 :  A ⊆ (L ＼ * (& (L ＼ * c)))
                 cc07 {z} az = subst (λ k → odef k z ) (
-                   begin  * c ≡⟨ sym ( L＼Lx=x cc08 ) ⟩
-                   L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) (sym *iso) ⟩
+                   begin  * c ≡⟨ sym ? ⟩
+                   L ＼ (L ＼ * c) ≡⟨ cong (λ k → L ＼ k ) ? ⟩
                    L ＼ * (& (L ＼ * c)) ∎ ) ( ac az ) where open ≡-Reasoning
         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) *iso cc05) ox  where
+           cc04 record { owner = o ; ao = ⟪ oo , A⊆L-o ⟫ ; ox = ox } = proj2 ( subst (λ k → odef k x) ? 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) (sym *iso) A⊆L-o) 
+                cc05 = ccx (& (L ＼ * o)) (P＼OS=CS top (subst (λ k → odef (OS top) k) (sym &iso) oo)) (subst (λ k → A ⊆ k) ? A⊆L-o) 
 
-CS∋x→Clx=x : {L x : HOD} → (top : Topology L) → CS top ∋ x → Cl top x ≡ x 
-CS∋x→Clx=x {L} {x} top cx = ==→o≡ record { eq→ = cc10 ; eq← = cc11 } where
+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) *iso ( cc (& x) cx (λ {z} xz → subst (λ k → odef k z) (sym *iso) xz  ) )
+    cc10 {y} ⟪ Ly , cc ⟫ = subst (λ k → odef k y) ? ( cc (& x) cx (λ {z} xz → subst (λ k → odef k z) ? 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 ) ⟫
 
@@ -136,7 +163,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 _ ) *iso  xy))
+is-sbp P {.(& (* _ ∩ * _))} (g∩ {x} {y} px px₁) xy = is-sbp P px (proj1 (subst (λ k → odef k _ ) ?  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)
@@ -173,48 +200,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 ) *iso (sym &iso) 0x ))
+    tp03 {x} 0x = ⊥-elim ( empty (* x) ( subst₂ (λ j k → odef j 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) (sym *iso) ul
+    tp01 {p} {q} op oq {x} ux =  record { b = b ; u⊆L = subst (λ k → k ⊆ L) ? ul
       ; 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 ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso ux ) )
+        px = subst (λ k → odef k x ) ? ( proj1 (subst (λ k → odef k _ ) ? ux ) )
         qx : odef (* (& q)) x
-        qx = subst (λ k → odef k x ) (sym *iso) ( proj2 (subst (λ k → odef k _ ) *iso ux ) )
+        qx = subst (λ k → odef k x ) ? ( proj2 (subst (λ k → odef k _ ) ? ux ) )
         b : Ordinal
         b = & (* (Base.b (op px)) ∩ * (Base.b (oq qx)))
         tp08 :  * b ⊆ * (& (p ∩ q) )
-        tp08 =  subst₂ (λ j k → j ⊆ k ) (sym *iso)  (sym *iso) (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) where
+        tp08 =  subst₂ (λ j k → j ⊆ k ) ?  ? (⊆∩-dist {(* (Base.b (op px)) ∩ * (Base.b (oq qx)))} {p} {q} tp09 tp10 ) 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 ) *iso tp11)
+             tp09 = ⊆∩-incl-1 {* (Base.b (op px))} {* (Base.b (oq qx))} {p} (subst (λ k → (* (Base.b (op px))) ⊆ k ) ? tp11)
              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 ) *iso tp12)
+             tp10 = ⊆∩-incl-2 {* (Base.b (oq qx))} {* (Base.b (op px))} {q} (subst (λ k → (* (Base.b (oq qx))) ⊆ k ) ? tp12)
         tp14 : odef (* (& (* (Base.b (op px)) ∩ * (Base.b (oq qx))))) x
-        tp14 = subst (λ k → odef k x ) (sym *iso) ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫
+        tp14 = subst (λ k → odef k x ) ? ⟪ Base.bx (op px) , Base.bx (oq qx) ⟫
         ul :  (p ∩ q) ⊆ L
-        ul = subst (λ k → k ⊆ L ) *iso (λ {z} pq →  (Base.u⊆L (op px)) (pz pq) )  where
+        ul = subst (λ k → k ⊆ L ) ? (λ {z} pq →  (Base.u⊆L (op px)) (pz pq) )  where
             pz : {z : Ordinal } → odef (* (& (p ∩ q))) z → odef (* (& p)) z
-            pz {z} pq = subst (λ k → odef k z ) (sym *iso) ( proj1 (subst (λ k → odef k _ ) *iso pq ) )
+            pz {z} pq = subst (λ k → odef k z ) ? ( proj1 (subst (λ k → odef k _ ) ? 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) *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 = subst (λ k → k ⊆ L) (sym *iso) tp04
-           ; sb = sb ; b⊆u = subst ( λ k → * b ⊆ k ) (sym *iso) 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 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  }
 
 -- Product Topology
 
@@ -240,16 +267,17 @@
 pbase⊆PL : {P Q : HOD} → (TP : Topology P) → (TQ : Topology Q) → {x : Ordinal } → BaseP TP Q x ∨ BaseQ P TQ x → odef (Power (ZFP P Q)) x
 pbase⊆PL {P} {Q} TP TQ {z} (case1 record { p = p ; op = op ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
     tp01 : odef (Power (ZFP P Q)) (& (ZFP (* p) Q))
-    tp01 w wz with subst (λ k → odef k w ) *iso wz
-    ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
-        tp03 : odef P a
-        tp03 =  os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
+    tp01 w wz = ?
+    -- tp01 w wz with subst (λ k → odef k w ) ? wz
+    -- ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) tp03 ) (subst (λ k → odef Q k ) (sym &iso) qb ) where
+    --     tp03 : odef P a
+    --     tp03 =  os⊆L TP (subst (λ k → odef (OS TP) k) (sym &iso) op) pa
 pbase⊆PL {P} {Q} TP TQ {z} (case2 record { q = q ; oq = oq ; prod = prod }) = subst (λ k → odef (Power (ZFP P Q)) k ) (sym prod) tp01  where
     tp01 : odef (Power (ZFP P Q)) (& (ZFP P (* q) ))
-    tp01 w wz with subst (λ k → odef k w ) *iso wz
-    ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 )  where
-        tp03 : odef Q b
-        tp03 =  os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb
+    tp01 w wz = ? -- with subst (λ k → odef k w ) ? wz
+    -- ... | ab-pair {a} {b} pa qb = ZFP→ (subst (λ k → odef P k ) (sym &iso) pa ) (subst (λ k → odef Q k ) (sym &iso) tp03 )  where
+    --     tp03 : odef Q b
+    --     tp03 =  os⊆L TQ (subst (λ k → odef (OS TQ) k) (sym &iso) oq) qb
 
 pbase : {P Q : HOD} → Topology P → Topology Q → HOD
 pbase {P} {Q} TP TQ = record { od = record { def = λ x → BaseP TP Q x ∨ BaseQ P TQ x } ; odmax = & (Power (ZFP P Q)) ; <odmax = tp00 } where
@@ -313,31 +341,33 @@
    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  ?
    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
-   CCX {X} os {x} ox with subst (λ k → odef k x) *iso ox
-   ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06  ⟫ where --  x ≡ & (L ＼ * z)
-      fip07 : z ≡ & (L ＼ * x)
-      fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L ＼ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where
-          fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) → odef (* z) x
-          fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) *iso not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥
-          ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ )
-          fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x)
-          fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw  , subst (λ k → ¬ odef k w) (sym *iso) fip10   ⟫ where
-             fip10 : ¬ (odef (L ＼ * z) w)
-             fip10 ⟪ Lw , nzw ⟫ = nzw zw
-      fip06 : odef (OS top) (& (L ＼ * x))
-      fip06 = os ( subst (λ k → odef (* X) k ) fip07 az )
-      fip05 : * x ⊆ L
-      fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw )
+   CCX {X} os {x} ox = ? -- with subst (λ k → odef k x) ? ox
+   -- ... | record { z = z ; az = az ; x=ψz = x=ψz } = ⟪ fip05 , fip06  ⟫ where --  x ≡ & (L ＼ * z)
+   --    fip07 : z ≡ & (L ＼ * x)
+   --    fip07 = subst₂ (λ j k → j ≡ k) &iso (cong (λ k → & ( L ＼ k )) (cong (*) (sym x=ψz))) ( cong (&) ( ==→o≡ record { eq→ = fip09 ; eq← = fip08 } )) where
+   --        fip08 : {x : Ordinal} → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x) → odef (* z) x
+   --        fip08 {x} ⟪ Lx , not ⟫ with subst (λ k → (¬ odef k x)) ? not -- ( odef L x ∧ odef (* z) x → ⊥) → ⊥
+   --        ... | Lx∧¬zx = ODC.double-neg-elim O ( λ nz → Lx∧¬zx ⟪ Lx , nz ⟫ )
+   --        fip09 : {x : Ordinal} → odef (* z) x → odef L x ∧ (¬ odef (* (& (L ＼ * z))) x)
+   --        fip09 {w} zw = ⟪ os⊆L top (os (subst (λ k → odef (* X) k) (sym &iso) az)) zw  , subst (λ k → ¬ odef k w) ? fip10   ⟫ where
+   --           fip10 : ¬ (odef (L ＼ * z) w)
+   --           fip10 ⟪ Lw , nzw ⟫ = nzw zw
+   --    fip06 : odef (OS top) (& (L ＼ * x))
+   --    fip06 = os ( subst (λ k → odef (* X) k ) fip07 az )
+   --    fip05 : * x ⊆ L
+   --    fip05 {w} xw = proj1 ( subst (λ k → odef k w) (trans (cong (*) x=ψz) ? ) xw )
+
    --
    --   X covres L means Intersection of (CX X) contains nothing
    --     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) RC＼ ) o∅
-   finCoverBase {X} ox oc with ODC.p∨¬p O (Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) o∅)
+   finCoverBase {X} ox oc with p∨¬p (Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) o∅)
    ... | case1 sb = sb
    ... | case2 ¬sb = ⊥-elim (¬¬cover fip25 fip20) where
        ¬¬cover : {z : Ordinal } →  odef L z → ¬ ( {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) z ))
@@ -347,19 +377,19 @@
        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 → Subbase j k ) ? 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)
+       fip26 : odef (* (CX ox))    (& (L ＼  * ( cover oc ( x∋minimal L (0<P→ne 0<L) ) )))
+       fip26 = subst (λ k → odef k (& (L ＼  * ( cover oc ( x∋minimal  L (0<P→ne 0<L) ) )) )) ?
           record { z = cover oc (x∋minimal L (0<P→ne 0<L)) ; az = P∋cover oc (x∋minimal L (0<P→ne 0<L))  ; x=ψz = refl }
        fip25 : odef L( FIP.limit fip (CCX ox) fip02 )
        fip25 = FIP.L∋limit fip (CCX ox) fip02 fip26
        fip20 : {y : Ordinal } → (Xy : odef (* X) y)  → ¬ ( odef (* y) ( FIP.limit fip (CCX ox) fip02 ))
        fip20 {y} Xy yl = proj2 fip21 yl where
            fip22 : odef (* (CX ox)) (& ( L ＼ * y ))
-           fip22 = subst (λ k → odef k (& ( L ＼ * y ))) (sym *iso) record { z = y ; az = Xy ; x=ψz = refl }
+           fip22 = subst (λ k → odef k (& ( L ＼ * y ))) ? 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 )
+           fip21 = subst (λ k → odef k ( FIP.limit fip (CCX ox) fip02 ) ) ? ( FIP.is-limit fip (CCX ox) fip02 fip22 )
    -- create HOD from Subbase ( finite intersection )
    finCoverSet : {X : Ordinal } → (x : Ordinal) →  Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x → HOD
    finCoverSet {X} x (gi rx) =  ( L ＼ * x ) , ( L ＼ * x  )
@@ -374,7 +404,7 @@
         fip60 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → Finite-∪ (* X) (& (finCoverSet {X} x sb))
         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
+           fip62 = cong₂ (λ j k → & (j , k )) ? ?
            fip61 : odef (Replace (* X) (_＼_ L) RC＼ ) 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,26 +412,26 @@
                fip33 : z1 ≡ & (L ＼ * x)
                fip33 = begin
                  z1 ≡⟨ sym &iso ⟩
-                 & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
-                 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
+                 & (* z1) ≡⟨ cong (&) ?  ⟩
+                 & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) ? ⟩
                  & (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
                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 ⟩ 
+                  (* (& (finCoverSet x sx)) ∪ * (& (finCoverSet y sy))) ≡⟨ cong₂ _∪_ ? ? ⟩ 
                   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) 
+   isCover1 {X} xo xcp = subst₂ (λ j k → j covers k ) ? (subst (λ k → L ＼ k ≡ L) ? ? ) -- L＼0=L) 
      (fip70 o∅ (finCoverBase xo xcp)) where
         fip70 : (x : Ordinal) → (sb : Subbase (Replace (* X) (λ z → L ＼ z) RC＼ ) x ) → (finCoverSet {X} x sb) covers (L ＼ * x)
         fip70 x (gi rx) = fip73 where
             fip73 : ((L ＼ * x) , (L ＼ * x)) covers (L ＼ * x)   -- obvious
             fip73 = record { cover = λ _ → & (L ＼ * x) ; P∋cover = λ _ → case1 refl 
-                ; isCover = λ {x} lt → subst (λ k → odef k x) (sym *iso) lt } 
+                ; isCover = λ {x} lt → subst (λ k → odef k x) ? 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} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where
+              (L ＼ k)) ? ( fip43 {_} {L} {* x} {* y} (fip71 (fip70 x sx)) (fip72 (fip70 y sy)) ) where
             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 } 
@@ -409,7 +439,7 @@
             fip72 {a} {b} {c} cov = record { cover = cover cov ; P∋cover = λ lt → case2 (P∋cover cov lt) 
                ; isCover = isCover cov } 
             fip45 : {L a b : HOD} → (L ＼ (a ∩ b)) ⊆ ( (L ＼ a) ∪  (L ＼ b))
-            fip45 {L} {a} {b} {x} Lab with ODC.∋-p O b (* x)
+            fip45 {L} {a} {b} {x} Lab with ∋-p  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 ) )
@@ -427,8 +457,6 @@
                 ... | case1 La = isCover ca La
                 ... | case2 Lb = isCover cb Lb
 
-open _==_
-
 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 )
@@ -438,28 +466,29 @@
    --   if 0 ≡ X then ¬ odef X x
    fip000 : {X x : Ordinal} (CX : * X ⊆ CS top) → ({y : Ordinal} → Subbase (* X) y → o∅ o< y) → ¬ odef (* X) x
    fip000 {X} {x} CX fip xx with trio< o∅ X
-   ... | tri< 0<X ¬b ¬c = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans (sym *iso) (cong (*) L=0)) o∅≡od∅ ) (sym &iso) 
+   ... | tri< 0<X ¬b ¬c = ¬∅∋ (subst₂ (λ j k → odef j k ) (trans (trans ? (cong (*) L=0)) ? ) (sym &iso) 
         ( cs⊆L top (subst (λ k → odef (CS top) 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∅ ≡⟨  ? ⟩ 
            od∅ ∎ ) (sym &iso) xx ) ) where open ≡-Reasoning
    ... | 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 ?
    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
-   OOX {X} cs {x} ox with subst (λ k → odef k x) *iso ox
-   ... | record { z = z ; az = az ; x=ψz = x=ψz } =  subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01))  where
-       comp01 : odef (* X) (& (* z))
-       comp01 = subst (λ k → odef (* X) k) (sym &iso) az
+   OOX {X} cs {x} ox = ? -- with subst (λ k → odef k x) ? ox
+   -- ... | record { z = z ; az = az ; x=ψz = x=ψz } =  subst (λ k → odef (OS top) k) (sym x=ψz) ( P＼CS=OS top (cs comp01))  where
+   --     comp01 : odef (* X) (& (* z))
+   --     comp01 = subst (λ k → odef (* X) k) (sym &iso) az
    --   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
@@ -471,9 +500,9 @@
       → (0<X : o∅ o< X ) →  NC CX fip 0<X
    has-intersection {X} CX fip 0<X =  intersection 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) )
+      Xe = x∋minimal (* X) (0<P→ne (subst (λ k → o∅ o< k) (sym &iso) 0<X) )
       no-cover : ¬ ( (* (OX CX)) covers L ) 
       no-cover cov = ⊥-elim (no-finite-cover (Compact.isCover compact (OOX CX) cov)) where
           -- construct Subase from Finite-∪
@@ -490,43 +519,43 @@
               fp22 : e ⊆ L
               fp22 {x} lt =  cs⊆L top (CX Xe) lt 
               fp21 : & e ≡ & (L ＼ * (& (L ＼ e)))
-              fp21 = cong (&) (trans (sym (L＼Lx=x fp22)) (cong (λ k → L ＼  k) (sym *iso)))
+              fp21 = cong (&) (trans (sym ?) (cong (λ k → L ＼  k) ?))
               fp23 : (L ＼ * (& (L ＼ e))) ⊆ (L ＼ Union (* o∅))
-              fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) o∅≡od∅ (sym &iso) (Own.ao lt )))) ⟫ 
+              fp23 {x} ⟪ Lx , _ ⟫ = ⟪ Lx , ( λ lt → ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ? (sym &iso) (Own.ao lt )))) ⟫ 
           fp02 t (fin-i {x} tx ) = record { i = x ; sb = gi fp03  ; t⊆i = fp24 } where
               -- we have a single cover x, L ＼ * x is single finite intersection
               fp24 : (L ＼ * x) ⊆ (L ＼ Union (* (& (* x , * x))))
-              fp24 {y} ⟪ Lx , not ⟫  = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) (sym *iso) fp25  ⟫ where
+              fp24 {y} ⟪ Lx , not ⟫  = ⟪ Lx , subst (λ k → ¬ odef (Union k) y) ? 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 )
+                   fp25 record { owner = .(& (* x)) ; ao = (case1 refl) ; ox = ox } = not (subst (λ k → odef k y) ? ox )
+                   fp25 record { owner = .(& (* x)) ; ao = (case2 refl) ; ox = ox } = not (subst (λ k → odef k y) ? ox )
               fp03 :  odef (* X) (& (L ＼ * x))  -- becase x is an element of  Replace (* X) (λ z → L ＼  z )
-              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
-                   fip34 : * z1 ⊆ L
-                   fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1
-                   fip33 : z1 ≡ & (L ＼ * x)
-                   fip33 = begin
-                     z1 ≡⟨ sym &iso ⟩
-                     & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
-                     & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) (sym *iso) ⟩
-                     & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
-                     & (L ＼ * x ) ∎ where open ≡-Reasoning
+              fp03 = ? -- with subst (λ k → odef k x ) ? tx
+              -- ... | record { z = z1 ; az = az1 ; x=ψz = x=ψz1 } = subst (λ k → odef (* X) k) fip33 az1 where
+              --      fip34 : * z1 ⊆ L
+              --      fip34 {w} wz1 = cs⊆L top (subst (λ k → odef (CS top) k) (sym &iso) (CX az1) ) wz1
+              --      fip33 : z1 ≡ & (L ＼ * x)
+              --      fip33 = begin
+              --        z1 ≡⟨ sym &iso ⟩
+              --        & (* z1) ≡⟨ cong (&) (sym  (L＼Lx=x fip34 )) ⟩
+              --        & (L ＼ ( L ＼ * z1)) ≡⟨ cong (λ k → & ( L ＼ k )) ? ⟩
+              --        & (L ＼ * (& ( L ＼ * z1))) ≡⟨ cong (λ k → & ( L ＼ * k )) (sym x=ψz1) ⟩
+              --        & (L ＼ * x ) ∎ where open ≡-Reasoning
           fp02 t (fin-∪ {tx} {ty} ux uy ) =  record { i = & (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))) ; sb = fp11  ; t⊆i = fp35 } where
               fp35 : (L ＼ * (& (* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy))))) ⊆ (L ＼ Union (* (& (* tx ∪ * ty))))
-              fp35 = subst₂ (λ j k →  (L ＼ j ) ⊆ (L ＼ Union k)) (sym *iso) (sym *iso) fp36  where
+              fp35 = subst₂ (λ j k →  (L ＼ j ) ⊆ (L ＼ Union k)) ? ? 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
+                      = ⊥-elim ( ¬∅∋ (subst₂ (λ j k → odef j k ) ?  (sym &iso) ao ))
+                  fp40 {z} {.(& (* _ , * _))} (fin-i {w} x) uz = fp41 x (subst (λ k → odef (Union k) z) ? 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 )
+                           os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) ? 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 } 
+                           os⊆L top (OOX CX (subst (λ k → odef (* (OX CX)) k) (sym &iso) x )) (subst (λ k → odef k z) ? ox )
+                  fp40 {z} {.(& (* _ ∪ * _))} (fin-∪ {x1} {y1} ftx fty) uz = ? -- with subst (λ k → odef (Union k) z ) ? 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 ux)) ∪ * (SB.i (fp02 ty uy)))) ⊆ (L ＼ Union (* tx ∪ * ty))
                   fp36 {z} ⟪ Lz , not ⟫ = ⟪ Lz , fp37 ⟫ where
                       fp37 : ¬ odef (Union (* tx ∪ * ty)) z 
@@ -534,27 +563,27 @@
                           fp38 : (L ＼  (* (SB.i (fp02 tx ux)))) ⊆ (L ＼ Union (* tx))
                           fp38 = SB.t⊆i (fp02 tx ux) 
                           fp39 : Union (* tx) ⊆  (* (SB.i (fp02 tx ux)))
-                          fp39 {w} txw with ∨L＼X {L} {* (SB.i (fp02 tx ux))} (fp40 ux txw)
-                          ... | case1 sb = sb
-                          ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) txw )
+                          fp39 {w} txw = ? -- with ∨L＼X {L} {* (SB.i (fp02 tx ux))} (fp40 ux 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 uy)))) ⊆ (L ＼ Union (* ty))
                           fp38 = SB.t⊆i (fp02 ty uy) 
                           fp39 : Union (* ty) ⊆  (* (SB.i (fp02 ty uy)))
-                          fp39 {w} tyw with ∨L＼X {L} {* (SB.i (fp02 ty uy))} (fp40 uy tyw)
-                          ... | case1 sb = sb
-                          ... | case2 lsb = ⊥-elim ( proj2 (fp38 lsb) tyw )
+                          fp39 {w} tyw = ? -- with ∨L＼X {L} {* (SB.i (fp02 ty uy))} (fp40 uy 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
+              fp04 {tx} {ty} = ? where -- cong (&) ( ==→o≡ record { eq→ = fp05 ; eq← = fp09 } ) where
                   fp05 : {x : Ordinal} → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x → odef (L ＼ * (& (* tx ∪ * ty))) x
-                  fp05 {x} lt with subst₂ (λ j k → odef (j ∩ k) x ) *iso *iso lt
-                  ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) (sym *iso) ⟪ Lx , fp06 ⟫  where
-                        fp06 : ¬ odef (* tx ∪ * ty) x 
-                        fp06 (case1 tx) = ¬tx tx
-                        fp06 (case2 ty) = ¬ty ty
+                  fp05 {x} lt = ? -- with subst₂ (λ j k → odef (j ∩ k) x ) ? ? lt
+                  -- ... | ⟪ ⟪ Lx , ¬tx ⟫ , ⟪ Ly , ¬ty ⟫ ⟫ = subst (λ k → odef (L ＼ k) x) ? ⟪ Lx , fp06 ⟫  where
+                  --       fp06 : ¬ odef (* tx ∪ * ty) x 
+                  --       fp06 (case1 tx) = ¬tx tx
+                  --       fp06 (case2 ty) = ¬ty ty
                   fp09 : {x : Ordinal} → odef (L ＼ * (& (* tx ∪ * ty))) x → odef (* (& (L ＼ * tx)) ∩ * (& (L ＼ * ty))) x
-                  fp09 {x} lt with subst (λ k → odef (L ＼ k) x) (*iso) lt
-                  ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) (sym *iso) (sym *iso) 
+                  fp09 {x} lt with subst (λ k → odef (L ＼ k) x) ? lt
+                  ... | ⟪ Lx , ¬tx∨ty ⟫ = subst₂ (λ j k → odef (j ∩ k) x ) ? ? 
                          ⟪ ⟪ Lx , ( λ tx → ¬tx∨ty (case1 tx)) ⟫ , ⟪ Lx , ( λ ty → ¬tx∨ty (case2 ty))  ⟫ ⟫ 
               fp11 : Subbase (* X) (& (L ＼ * (& ((* (SB.i (fp02 tx ux)) ∪ * (SB.i (fp02 ty uy)))))))
               fp11 = subst (λ k → Subbase (* X) k ) fp04 ( g∩ (SB.sb (fp02 tx ux)) (SB.sb (fp02 ty uy )) ) 
@@ -568,7 +597,7 @@
           sb : SB (Compact.finCover compact (OOX CX) cov)
           sb = fp02 fp01 (Compact.isFinite compact (OOX CX) cov)
           no-finite-cover : ¬ ( (* (Compact.finCover compact (OOX CX) cov)) covers L ) 
-          no-finite-cover fcovers = ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where
+          no-finite-cover fcovers = ? where -- ⊥-elim ( o<¬≡ (cong (&) (sym (==→o≡ f22))) f25 ) where
                f23 : (L ＼ * (SB.i sb)) ⊆ ( L ＼  Union (* (Compact.finCover compact (OOX CX) cov)))
                f23 = SB.t⊆i sb
                f22 : (L ＼  Union (* (Compact.finCover compact (OOX CX) cov))) =h= od∅
@@ -581,7 +610,7 @@
                   & (L ＼  Union (* (Compact.finCover compact (OOX CX) cov)))  ∎  ) where open o≤-Reasoning O
       -- if we have no cover, we can consruct NC
       intersection : NC CX fip 0<X
-      intersection with ODC.p∨¬p O (NC CX fip 0<X)
+      intersection with p∨¬p (NC CX fip 0<X)
       ... | case1 nc = nc 
       ... | case2 ¬nc = ⊥-elim ( no-cover record { cover = λ Lx → & (L ＼ coverf Lx) ; P∋cover = fp22 ; isCover = fp23 } ) where
           coverSet : {x : Ordinal} → odef L x → HOD
@@ -590,23 +619,23 @@
           fp17 : {x : Ordinal} → (Lx : odef L x ) → ¬ ( coverSet Lx =h= od∅ )
           fp17 {x} Lx eq = ⊥-elim (¬nc record { x = x ; yx = fp19 } ) where
              fp19 : {y : Ordinal} → odef (* X) y → odef (* y) x
-             fp19 {y} Xy with ∨L＼X {L} {* y} {x} Lx
-             ... | case1 yx = yx
-             ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where
-                fp20 : odef (* X) y ∧ odef (L ＼ * y) x
-                fp20 = ⟪ Xy , lyx ⟫
+             fp19 {y} Xy = ? -- with ∨L＼X {L} {* y} {x} Lx
+             -- ... | case1 yx = yx
+             -- ... | case2 lyx = ⊥-elim ( ¬x<0 {y} ( eq→ eq fp20 )) where
+             --    fp20 : odef (* X) y ∧ odef (L ＼ * y) x
+             --    fp20 = ⟪ Xy , lyx ⟫
           coverf : {x : Ordinal} → (Lx : odef L x ) → HOD
-          coverf Lx =  ODC.minimal O (coverSet Lx) (fp17 Lx)
+          coverf Lx =  minimal (coverSet Lx) (fp17 Lx)
           fp22 :  {x : Ordinal} (lt : odef L x) → odef (* (OX CX)) (& (L ＼ coverf lt))
-          fp22 {x} Lx = subst (λ k → odef k (& (L ＼ coverf Lx ))) (sym *iso) record { z = _ ; az = fp25 ; x=ψz = fp24   } where
+          fp22 {x} Lx = subst (λ k → odef k (& (L ＼ coverf Lx ))) ? record { z = _ ; az = fp25 ; x=ψz = fp24   } where
              fp24 : & (L ＼ coverf Lx) ≡ & (L ＼ * (& (coverf Lx)))
-             fp24 = cong (λ k → & ( L ＼ k )) (sym *iso)
+             fp24 = cong (λ k → & ( L ＼ k )) ?
              fp25 : odef (* X) (& (coverf Lx))
-             fp25 = proj1 ( ODC.x∋minimal O (coverSet Lx) (fp17 Lx) )
+             fp25 = proj1 ( x∋minimal (coverSet Lx) (fp17 Lx) )
           fp23 :  {x : Ordinal} (lt : odef L x) → odef (* (& (L ＼ coverf lt))) x
-          fp23 {x} Lx = subst (λ k → odef k x) (sym *iso) ⟪ Lx , fp26 ⟫  where
+          fp23 {x} Lx = subst (λ k → odef k x) ? ⟪ Lx , fp26 ⟫  where
              fp26 : ¬ odef (coverf Lx) x
-             fp26 = subst (λ k → ¬ odef k x ) *iso (proj2 (proj2 ( ODC.x∋minimal O (coverSet Lx) (fp17 Lx) ))  )
+             fp26 = subst (λ k → ¬ odef k x ) ? (proj2 (proj2 ( x∋minimal (coverSet Lx) (fp17 Lx) ))  )
    limit : {X : Ordinal} (CX : * X ⊆ CS top) (fip : {x : Ordinal} → Subbase (* X) x → o∅ o< x) → Ordinal
    limit {X} CX fip with trio< X o∅ 
    ... | tri< a ¬b ¬c = ⊥-elim ( ¬x<0 a )
@@ -647,7 +676,7 @@
     f1 : {p q : HOD} → Power P ∋ q → NF ∋ p → p ⊆ q → NF ∋ q
     f1 {p} {q} Pq Np p⊆q = record { u = Neighbor.u Np ; ou = Neighbor.ou Np ; ux = Neighbor.ux Np ; v⊆P = Pq _ ; u⊆v = f11 } where
         f11 :  * (Neighbor.u Np) ⊆ * (& q)
-        f11 {x} ux = subst (λ k → odef k x ) (sym *iso) ( p⊆q (subst (λ k → odef k x) *iso (Neighbor.u⊆v Np ux)) )
+        f11 {x} ux = subst (λ k → odef k x ) ? ( p⊆q (subst (λ k → odef k x) ? (Neighbor.u⊆v Np ux)) )
     f2 : {p q : HOD} → NF ∋ p → NF ∋ q → Power P ∋ (p ∩ q) → NF ∋ (p ∩ q)
     f2 {p} {q} Np Nq Ppq = record { u = upq ; ou = ou ; ux = ux ; v⊆P = Ppq _ ; u⊆v = f20 } where
          upq : Ordinal
@@ -655,16 +684,16 @@
          ou : odef (OS TP) upq
          ou = o∩ TP (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Np)) (subst (λ k → odef (OS TP) k) (sym &iso) (Neighbor.ou Nq))
          ux :  odef (* upq) x
-         ux = subst ( λ k → odef k x ) (sym *iso) ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫
+         ux = subst ( λ k → odef k x ) ? ⟪ Neighbor.ux Np , Neighbor.ux Nq ⟫
          f20 : * upq ⊆ * (& (p ∩ q))
-         f20 = subst₂ (λ j k → j ⊆ k ) (sym *iso) (sym *iso) ( λ {x} pq 
-           → ⟪ subst (λ k → odef k x) *iso (Neighbor.u⊆v Np (proj1 pq))  , subst (λ k → odef k x) *iso (Neighbor.u⊆v Nq (proj2 pq)) ⟫  )
+         f20 = subst₂ (λ j k → j ⊆ k ) ? ? ( λ {x} pq 
+           → ⟪ subst (λ k → odef k x) ? (Neighbor.u⊆v Np (proj1 pq))  , subst (λ k → odef k x) ? (Neighbor.u⊆v Nq (proj2 pq)) ⟫  )
 
 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 ) *iso pqx
-... | ⟪ px , qx ⟫ = Pp _ (subst (λ k → odef k x) (sym *iso) px )
+CAP P {p} {q} Pp Pq x pqx with subst (λ k → odef k x ) ? pqx
+... | ⟪ 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) *iso vx
+NEG P {p} Pp x vx with subst (λ k → odef k x) ? vx
 ... | ⟪ Px , npx ⟫ = Px
 
diff -r 6752e2ff4dc6 -r 32001d93755b src/VL.agda
--- a/src/VL.agda	Fri Jun 28 17:41:43 2024 +0900
+++ b/src/VL.agda	Fri Jun 28 20:55:38 2024 +0900
@@ -1,35 +1,51 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+open import Level
+open import Ordinals
+open import logic
+open import Relation.Nullary
+
 open import Level
 open import Ordinals
-module VL {n : Level } (O : Ordinals {n}) where
+import HODBase
+import OD
+open import Relation.Nullary
+module VL {n : Level } (O : Ordinals {n} ) (HODAxiom : HODBase.ODAxiom O)  (ho< : OD.ODAxiom-ho< O HODAxiom ) where
+
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Data.Empty
+
+import OrdUtil
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+import ODUtil
 
 open import logic
-import OD 
-open import Relation.Nullary 
-open import Relation.Binary 
-open import Data.Empty 
-open import Relation.Binary
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-import BAlgebra 
-open BAlgebra O
-open inOrdinal O
-import OrdUtil
-import ODUtil
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
---  open Ordinals.IsNext isNext
+open import nat
+
 open OrdUtil O
-open ODUtil O
+open ODUtil O HODAxiom  ho<
 
-open OD O
-open OD.OD
-open ODAxiom odAxiom
--- import ODC
 open _∧_
 open _∨_
 open Bool
-open HOD
+
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+open import Relation.Binary
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
+
 
 -- The cumulative hierarchy 
 --    V 0 := ∅ 
@@ -59,15 +75,15 @@
      β  : Ordinal
      ov : odef (TransFinite  V1 β) x 
 
-Vn∅ : Vn
-Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? }
+-- Vn∅ : Vn
+-- Vn∅ = record { x = o∅ ; β = o∅ ; ov = ? }
 
-vsuc : Vn → Vn
-vsuc v = ?
+-- vsuc : Vn → Vn
+-- vsuc v = ?
 
-v< : Vn → Vn → Set n
-v< x y = ?
+-- v< : Vn → Vn → Set n
+-- v< x y = ?
 
-IsVOrd : IsOrdinals Vn Vn∅ vsuc ?
-IsVOrd = ?
+-- IsVOrd : IsOrdinals Vn Vn∅ vsuc ?
+-- IsVOrd = ?
 
diff -r 6752e2ff4dc6 -r 32001d93755b src/filter-util.agda
--- a/src/filter-util.agda	Fri Jun 28 17:41:43 2024 +0900
+++ b/src/filter-util.agda	Fri Jun 28 20:55:38 2024 +0900
@@ -1,45 +1,55 @@
-{-# 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 filter-util {n : Level } (O : Ordinals {n})   where
+import HODBase
+import OD
+open import Relation.Nullary
+module filter-util {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 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 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  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
 
-import ODC
-open ODC O
+open HODBase.HOD
 
-open import filter O
-open import ZProduct O
--- open import maximum-filter O
+open AxiomOfChoice AC
+open import ODC O HODAxiom AC as ODC
+
+open import filter O HODAxiom ho< AC
+open import ZProduct O HODAxiom ho<
 
 open Filter
 
 filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) →  {x : HOD} → filter F ∋ x  →  { z : Ordinal } 
     → odef x z → odef (ZFP P Q) z
-filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (subst (λ k → odef k z) (sym *iso) xz )
+filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (subst (λ k → odef k z) ? xz )
 
 rcp :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) P (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx))
 rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly }
@@ -55,62 +65,62 @@
     isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q
     isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) 
     fp00 : FP ⊆ Power P 
-    fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw
-    ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
+    fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) ? ) xw
+    ... | t = ? -- record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
     f0 :  {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
     f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q 
     f1 :  {p q : HOD} → Power P ∋ q → FP ∋ p → p ⊆ q → FP ∋ q
     f1 {p} {q} Pq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP q Q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj1 } where
        PQq : Power (ZFP P Q) ∋ ZFP q Q
-       PQq z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq )
+       PQq z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans ? (cong (λ k → ZFP k Q) ?)) zpq )
        q⊆P : q ⊆ P
-       q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw )
+       q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym ?) qw )
        p⊆P : p ⊆ P
        p⊆P {w} pw = q⊆P (p⊆q pw)
        p=proj1 : & p ≡ & (ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az)))
        p=proj1 = x=ψz
        p⊆ZP : (* z) ⊆ ZFP p Q
-       p⊆ZP = subst (λ k → (* z) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP 
+       p⊆ZP = subst (λ k → (* z) ⊆ ZFP k Q) (sym ?) ZP-proj1⊆ZFP 
        ty05 : filter F ∋  ZFP p Q
-       ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP
+       ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) ? wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP
        ty06 : ZFP p Q ⊆ ZFP q Q
        ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
        fp01 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q
        fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq
        q=proj1 : & q ≡ & (ZP-proj1 P Q (* (& (ZFP q Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06))))
-       q=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) q⊆P *iso )
+       q=proj1 = ? -- cong (&) (ZP-proj1=rev (zp2 pqa) q⊆P *iso )
     f2 : {p q : HOD} → FP ∋ p → FP ∋ q → Power P ∋ (p ∩ q) → FP ∋ (p ∩ q)
     f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq 
          = record { z = _ ; az = ty50 ; x=ψz = pq=proj1 } where
        p⊆P : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
             (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ P
-       p⊆P {zp} {p} fzp p=proj1 {x} px with subst (λ k → odef k x) (&≡&→≡ p=proj1) px
-       ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
+       p⊆P {zp} {p} fzp p=proj1 {x} px with subst (λ k → odef k x) ? px
+       ... | t = ? -- record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
        x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
             (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP p Q
-       x⊆pxq {zp} {p} fzp p=proj1 = subst (λ k → (* zp) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP
+       x⊆pxq {zp} {p} fzp p=proj1 = subst (λ k → (* zp) ⊆ ZFP k Q) (sym ?) ZP-proj1⊆ZFP
        ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q)
        ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
          pqz :  odef (ZFP (p ∩ q) Q)  z
-         pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) ))  xz
+         pqz = ? -- subst (λ k → odef k z ) (trans ? (sym (proj1 ZFP∩) ))  xz
          pqz1 : odef P (zπ1 pqz)
          pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz))
          pqz2 : odef Q (zπ2 pqz)
          pqz2 = zp2 pqz
        ty53 : filter F ∋ ZFP p Q
        ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp)
-         (subst (λ k → odef k z) *iso wz))
-         (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
+         ?)
+         ? ? -- (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
        ty52 : filter F ∋ ZFP q Q
        ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq)
-         (subst (λ k → odef k z) *iso wz))
-         (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq)
+         ?)
+         ? (x⊆pxq fzq x=ψzq)
        ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
        ty51 = filter2 F ty53 ty52 ty54
        ty50 : filter F ∋ ZFP (p ∩ q) Q
-       ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51
+       ty50 = subst (λ k → filter F ∋ k ) ? ty51
        pq=proj1 : & (p ∩ q) ≡ & (ZP-proj1 P Q (* (& (ZFP (p ∩ q) Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50)))
-       pq=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) (sym *iso) pqx)) *iso )
+       pq=proj1 = ? -- cong (&) (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) ? pqx)) *iso )
 
 Filter-Proj1-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a )
       → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
@@ -119,26 +129,26 @@
        FP = Filter-Proj1 pqa F
        ty60 : ¬ (filter FP ∋ od∅)
        ty60 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim (ultra-filter.proper UF 
-          (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) (*iso) x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where
+          (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) ? x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where
            ty61 : * z ⊆  od∅
-           ty61 {x} lt = ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj1-0 (sym (&≡&→≡ x=ψz)))) *iso)  lt ))
+           ty61 {x} lt = ? -- ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj1-0 (sym ?))) *iso)  lt ))
        ty62 :  {p : HOD} → Power P ∋ p → Power P ∋ (P ＼ p) → (filter (Filter-Proj1 pqa F) ∋ p) ∨ (filter (Filter-Proj1 pqa F) ∋ (P ＼ p))
        ty62 {p} Pp NEGP = uf05  where
              p⊆P : p ⊆ P
-             p⊆P {z} px = Pp _ (subst (λ k → odef k z) (sym *iso) px)
+             p⊆P {z} px = Pp _ (subst (λ k → odef k z) ? px)
              mp : HOD
              mp = ZFP p Q 
              uf03 : Power (ZFP P Q) ∋  mp
-             uf03 x xz with subst (λ k → odef k x ) *iso xz
-             ... | ab-pair ax by = ab-pair (p⊆P ax) by
+             uf03 x xz with subst (λ k → odef k x ) ? xz
+             ... | t = ? -- ab-pair ax by = ab-pair (p⊆P ax) by
              uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mp)
-             uf04 x xz = proj1 (subst (λ k → odef k x) *iso xz)
+             uf04 x xz = ? -- proj1 (subst (λ k → odef k x) *iso xz)
              uf02 : (filter F ∋ mp) ∨ (filter F ∋ (ZFP P Q ＼ mp))
              uf02 = ultra-filter.ultra UF uf03 uf04
              uf05 : (filter FP ∋ p) ∨ (filter FP ∋ (P ＼ p))
              uf05 with uf02
-             ... | case1 fp  = case1 record { z = _ ; az = fp  ; x=ψz = cong (&) (ZP-proj1=rev (zp2 pqa) p⊆P *iso)  }
-             ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = cong (&) (ZP-proj1=rev (zp2 pqa) proj1 (trans *iso (proj1 ZFP\Q)) )  } 
+             ... | case1 fp  = case1 record { z = _ ; az = fp  ; x=ψz = ?  }
+             ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = ? }
 
 rcq :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) Q (λ x fx → ZP-proj2 P Q x (filter-⊆ F fx))
 rcq {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP2.bb ly }
@@ -159,62 +169,62 @@
     isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q
     isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) 
     fp00 : FQ ⊆ Power Q 
-    fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw
-    ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb
+    fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) ? ) xw
+    ... | t = ? -- record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb
     f0 :  {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
     f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q 
     f1 :  {p q : HOD} → Power Q ∋ q → FQ ∋ p → p ⊆ q → FQ ∋ q
     f1 {p} {q} Qq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP P q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj2 } where
        PQq : Power (ZFP P Q) ∋ ZFP P q
-       PQq z zpq = isQ→PxQ {* (& q)}  (Qq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP P k) (sym *iso))) zpq ) 
+       PQq z zpq = isQ→PxQ {* (& q)}  (Qq _) ( subst (λ k → odef k z ) ? zpq ) 
        q⊆P : q ⊆ Q
-       q⊆P {w} qw = Qq _ (subst (λ k → odef k w ) (sym *iso) qw )
+       q⊆P {w} qw = Qq _ (subst (λ k → odef k w ) ? qw )
        p⊆P : p ⊆ Q
        p⊆P {w} pw = q⊆P (p⊆q pw)
        p=proj2 : & p ≡ & (ZP-proj2 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az)))
        p=proj2 = x=ψz
        p⊆ZP : (* z) ⊆ ZFP P p
-       p⊆ZP = subst (λ k → (* z) ⊆ ZFP P k ) (sym (&≡&→≡ p=proj2)) ZP-proj2⊆ZFP 
+       p⊆ZP = subst (λ k → (* z) ⊆ ZFP P k ) (sym ?) ZP-proj2⊆ZFP 
        ty05 : filter F ∋  ZFP P p
-       ty05 = filter1 F (λ z wz → isQ→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP
+       ty05 = filter1 F (λ z wz → isQ→PxQ p⊆P ?) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP
        ty06 : ZFP P p ⊆ ZFP P q
        ty06 (ab-pair wp wq ) = ab-pair wp (p⊆q wq) 
        fp01 : filter F ∋ ZFP P p → ZFP P p ⊆ ZFP P q → filter F ∋ ZFP P q
        fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq
        q=proj2 : & q ≡ & (ZP-proj2 P Q (* (& (ZFP P q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06))))
-       q=proj2 = cong (&) (ZP-proj2=rev (zp1 pqa) q⊆P *iso )
+       q=proj2 = ? -- cong (&) (ZP-proj2=rev (zp1 pqa) q⊆P *iso )
     f2 : {p q : HOD} → FQ ∋ p → FQ ∋ q → Power Q ∋ (p ∩ q) → FQ ∋ (p ∩ q)
     f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq 
          = record { z = _ ; az = ty50 ; x=ψz = pq=proj2 } where
        p⊆Q : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
             (ZP-proj2 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ Q
-       p⊆Q {zp} {p} fzp p=proj2 {x} px with subst (λ k → odef k x) (&≡&→≡ p=proj2) px
-       ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb
+       p⊆Q {zp} {p} fzp p=proj2 {x} px with subst (λ k → odef k x) ? px
+       ... | t = ? -- record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb
        x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
             (ZP-proj2 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP P p 
-       x⊆pxq {zp} {p} fzp p=proj2 = subst (λ k → (* zp) ⊆ ZFP P k ) (sym (&≡&→≡ p=proj2)) ZP-proj2⊆ZFP
+       x⊆pxq {zp} {p} fzp p=proj2 = subst (λ k → (* zp) ⊆ ZFP P k ) (sym ?) ZP-proj2⊆ZFP
        ty54 : Power (ZFP P Q) ∋ (ZFP P p  ∩ ZFP P q )
        ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
          pqz :  odef (ZFP P (p ∩ q) )  z
-         pqz = subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) ))  xz
+         pqz = ? --- subst (λ k → odef k z ) (trans *iso (sym (proj2 ZFP∩) ))  xz
          pqz1 : odef P (zπ1 pqz)
          pqz1 = zp1 pqz
          pqz2 : odef Q (zπ2 pqz)
          pqz2 = p⊆Q fzp x=ψzp (proj1 (zp2 pqz))
        ty53 : filter F ∋ ZFP P p 
        ty53 = filter1 F (λ z wz → isQ→PxQ (p⊆Q fzp x=ψzp)
-         (subst (λ k → odef k z) *iso wz))
-         (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
+         ?)
+         ? (x⊆pxq fzp x=ψzp)
        ty52 : filter F ∋ ZFP P q 
        ty52 = filter1 F (λ z wz → isQ→PxQ (p⊆Q fzq x=ψzq)
-         (subst (λ k → odef k z) *iso wz))
-         (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq)
+         ?)
+         ? (x⊆pxq fzq x=ψzq)
        ty51 : filter F ∋ ( ZFP P p ∩ ZFP P q  )
        ty51 = filter2 F ty53 ty52 ty54
        ty50 : filter F ∋ ZFP P (p ∩ q) 
-       ty50 = subst (λ k → filter F ∋ k ) (sym (proj2 ZFP∩)) ty51
+       ty50 = subst (λ k → filter F ∋ k ) (sym ?) ty51
        pq=proj2 : & (p ∩ q) ≡ & (ZP-proj2 P Q (* (& (ZFP P (p ∩ q) ))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50)))
-       pq=proj2 = cong (&) (ZP-proj2=rev (zp1 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) (sym *iso) pqx)) *iso )
+       pq=proj2 = ? -- cong (&) (ZP-proj2=rev (zp1 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) ? pqx)) *iso )
 
 Filter-Proj2-UF : {P Q a : HOD } → (pqa : ZFP P Q ∋ a )
       → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
@@ -223,26 +233,26 @@
        FQ = Filter-Proj2 pqa F
        ty60 : ¬ (filter FQ ∋ od∅)
        ty60 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim (ultra-filter.proper UF 
-          (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) (*iso) x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where
+          (filter1 F (λ x x<0 → ⊥-elim (¬x<0 (subst (λ k → odef k x) ? x<0))) (subst (λ k → odef (filter F) k ) (sym &iso) az) ty61 )) where
            ty61 : * z ⊆  od∅
-           ty61 {x} lt = ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj2-0 (sym (&≡&→≡ x=ψz)))) *iso)  lt ))
+           ty61 {x} lt = ⊥-elim (¬x<0 (subst (λ k → odef k x) (trans (cong (*) (ZP-proj2-0 (sym ?))) ?)  lt ))
        ty62 :  {p : HOD} → Power Q ∋ p → Power Q ∋ (Q ＼ p) → (filter (Filter-Proj2 pqa F) ∋ p) ∨ (filter (Filter-Proj2 pqa F) ∋ (Q ＼ p))
        ty62 {p} Qp NEGQ = uf05  where
              p⊆Q : p ⊆ Q
-             p⊆Q {z} px = Qp _ (subst (λ k → odef k z) (sym *iso) px)
+             p⊆Q {z} px = Qp _ (subst (λ k → odef k z) ? px)
              mq : HOD
              mq = ZFP P p  
              uf03 : Power (ZFP P Q) ∋  mq
-             uf03 x xz with subst (λ k → odef k x ) *iso xz
-             ... | ab-pair ax by = ab-pair ax (p⊆Q by) 
+             uf03 x xz with subst (λ k → odef k x ) ? xz
+             ... | t = ? -- ab-pair ax by = ab-pair ax (p⊆Q by) 
              uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mq)
-             uf04 x xz = proj1 (subst (λ k → odef k x) *iso xz)
+             uf04 x xz = ? -- proj1 (subst (λ k → odef k x) *iso xz)
              uf02 : (filter F ∋ mq) ∨ (filter F ∋ (ZFP P Q ＼ mq))
              uf02 = ultra-filter.ultra UF uf03 uf04
              uf05 : (filter FQ ∋ p) ∨ (filter FQ ∋ (Q ＼ p))
              uf05 with uf02
-             ... | case1 fp  = case1 record { z = _ ; az = fp  ; x=ψz = cong (&) (ZP-proj2=rev (zp1 pqa) p⊆Q *iso)  }
-             ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = cong (&) (ZP-proj2=rev (zp1 pqa) proj1 (trans *iso (proj2 ZFP\Q)) )  } 
+             ... | case1 fp  = case1 record { z = _ ; az = fp  ; x=ψz = cong (&) ?  }
+             ... | case2 fnp = case2 record { z = _ ; az = fnp ; x=ψz = cong (&) ?  } 
 
 rcf :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx))
 rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly }
@@ -257,14 +267,14 @@
     fqp<P : fqp ⊆ Power (ZFP Q P)
     fqp<P {z} record { z = x ; az = fx ; x=ψz = x=ψz } w xw = 
          ZPmirror⊆ZFPBA P Q (* x) (filter-⊆ F (subst (λ k → odef (filter F) k) (sym &iso) fx )) 
-            (subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw) 
+            (subst (λ k → odef k w) ? xw) 
     f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q
     f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 
       ; x=ψz = fis05 }  where
          fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
          fis00 = filter1 F 
          q⊆ZQP : q ⊆ ZFP Q P
-         q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) (sym *iso) qx) 
+         q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) ? qx) 
          p⊆ZQP : p ⊆ ZFP Q P
          p⊆ZQP {z} px = q⊆ZQP (p⊆q px)
          fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fqp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fqp))))
@@ -272,26 +282,26 @@
          fig03 : filter F ∋  ZPmirror Q P p p⊆ZQP
          fig03 with Replaced1.az fqp 
          ... | fz = subst (λ k → odef (filter F) k ) fig07  fz where
-             fig07 :  Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (subst (λ k → def (HOD.od k) x ) (sym *iso) (p⊆q px))))
-             fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) )))))
+             fig07 :  Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (subst (λ k → ? ) ? (p⊆q px))))
+             fig07 = trans (sym &iso) ( sym (cong (&) ?))
          fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP
-         fig01 x xz  = ZPmirror⊆ZFPBA Q P q q⊆ZQP (subst (λ k → odef k x) *iso xz)
+         fig01 x xz  = ZPmirror⊆ZFPBA Q P q q⊆ZQP (subst (λ k → odef k x) ? xz)
          fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP
          fis04 = ZPmirror-⊆ p⊆q
          fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP)))
              (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04))))
-         fis05 = cong (&) (sym ( ZPmirror-rev (sym *iso) ))
+         fis05 = cong (&) (sym ?)
     f2 : {p q : HOD} → fqp ∋ p → fqp ∋ q → Power (ZFP Q P) ∋ (p ∩ q) → fqp ∋ (p ∩ q)
     f2 {p} {q} fp fq QPpq = record { z = _ ; az = fis12 {ZPmirror Q P p p⊆ZQP} {ZPmirror Q P q q⊆ZQP} fig03 fig04 fig01
       ; x=ψz = fis05 }  where
          fis12 : {p q : HOD} → filter F ∋ p → filter F ∋ q → Power (ZFP P Q) ∋ (p ∩ q) → filter F ∋ (p ∩ q)
          fis12 {p} {q} fp fq PQpq = filter2 F fp fq PQpq
          p⊆ZQP : p ⊆ ZFP Q P
-         p⊆ZQP {z} px = fqp<P fp _ (subst (λ k → odef k z) (sym *iso) px)
+         p⊆ZQP {z} px = fqp<P fp _ (subst (λ k → odef k z) ? px)
          q⊆ZQP : q ⊆ ZFP Q P
-         q⊆ZQP {z} qx = fqp<P fq _ (subst (λ k → odef k z) (sym *iso) qx)
+         q⊆ZQP {z} qx = fqp<P fq _ (subst (λ k → odef k z) ? qx)
          pq⊆ZQP : (p ∩ q) ⊆ ZFP Q P
-         pq⊆ZQP {z} pqx = QPpq _ (subst (λ k → odef k z) (sym *iso) pqx)
+         pq⊆ZQP {z} pqx = QPpq _ (subst (λ k → odef k z) ? pqx)
          fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fp))))
          fig06 = Replaced1.x=ψz fp
          fig09 : & q ≡ & (ZPmirror P Q (* (Replaced1.z fq)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fq))))
@@ -299,16 +309,16 @@
          fig03 : filter F ∋  ZPmirror Q P p p⊆ZQP
          fig03 = subst (λ k → odef (filter F) k ) fig07 ( Replaced1.az fp )  where
              fig07 :  Replaced1.z fp ≡ & (ZPmirror Q P p p⊆ZQP )
-             fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) )))))
+             fig07 = trans (sym &iso) ( sym (cong (&) ?))
          fig04 : filter F ∋  ZPmirror Q P q q⊆ZQP
          fig04 = subst (λ k → odef (filter F) k ) fig08 ( Replaced1.az fq )  where
              fig08 :  Replaced1.z fq ≡ & (ZPmirror Q P q q⊆ZQP )
-             fig08 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig09) )))))
+             fig08 = trans (sym &iso) ( sym (cong (&) ?))
          fig01 : Power (ZFP P Q) ∋ ( ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP )
-         fig01 x xz  = ZPmirror⊆ZFPBA Q P q q⊆ZQP (proj2 (subst (λ k → odef k x) *iso xz))
+         fig01 x xz  = ZPmirror⊆ZFPBA Q P q q⊆ZQP ?
          fis05 : & (p ∩ q) ≡ & (ZPmirror P Q (* (& (ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP))) 
              (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis12 fig03 fig04 fig01) )))
-         fis05 = cong (&) (sym ( ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} (trans ZPmirror-∩ (sym *iso) ) ))
+         fis05 = ? -- cong (&) (sym ( ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} ? ))
 
 Filter-sym-UF : {P Q : HOD } → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
@@ -318,27 +328,26 @@
      uf00 : ¬ (Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf  F) ∋ od∅)
      uf00 record { z = z ; az = az ; x=ψz = x=ψz } = ⊥-elim ( ultra-filter.proper UF (subst (λ k → odef (filter F) k) uf10 az )) where
          uf10 : z ≡ & od∅
-         uf10 = ZPmirror-0 (sym (&≡&→≡ x=ψz))
+         uf10 = ZPmirror-0 (sym ?)
      uf01 : {p : HOD} → Power (ZFP Q P) ∋ p → Power (ZFP Q P) ∋ (ZFP Q P ＼ p) →
             (filter FQP ∋ p) ∨ (filter FQP ∋ (ZFP Q P ＼ p))
      uf01 {p} QPp NEGP = uf05  where
          p⊆ZQP : p ⊆ ZFP Q P
-         p⊆ZQP {z} px = QPp _ (subst (λ k → odef k z) (sym *iso) px)
+         p⊆ZQP {z} px = QPp _ (subst (λ k → odef k z) ? px)
          mp : HOD
          mp = ZPmirror Q P p p⊆ZQP
          uf03 : Power (ZFP P Q) ∋  mp
-         uf03 x xz = ZPmirror⊆ZFPBA Q P p p⊆ZQP (subst (λ k → odef k x) *iso xz)
+         uf03 x xz = ZPmirror⊆ZFPBA Q P p p⊆ZQP ?
          uf04 : Power (ZFP P Q) ∋ (ZFP P Q ＼ mp)
-         uf04 x xz = proj1 (subst (λ k → odef k x) *iso xz)
+         uf04 x xz = proj1 ?
          uf02 : (filter F ∋ mp) ∨ (filter F ∋ (ZFP P Q ＼ mp))
          uf02 = ultra-filter.ultra UF uf03 uf04
          uf05 : (filter FQP ∋ p) ∨ (filter FQP ∋ (ZFP Q P ＼ p))
          uf05 with uf02
-         ... | case1 fp  = case1 record { z = _ ; az = fp   ; x=ψz = cong (&) (sym ( ZPmirror-rev (sym *iso) )) }
-         ... | case2 fnp = case2 record { z = _ ; az = uf06 ; x=ψz = cong (&) (sym ( ZPmirror-rev (sym *iso) )) } where
+         ... | case1 fp  = case1 record { z = _ ; az = fp   ; x=ψz = ? }
+         ... | case2 fnp = case2 record { z = _ ; az = uf06 ; x=ψz = ? } where
                uf06 : odef (filter F) (& (ZPmirror Q P (ZFP Q P ＼ p) proj1 ))
-               uf06 = subst (λ k → odef (filter F)  k) (cong (&) (sym (trans ZPmirror-neg 
-                  (cong (λ k → k ＼ (ZPmirror Q P p (λ {z} px → QPp z (subst (λ k → OD.def (HOD.od k) z) (sym *iso) px)))) ZPmirror-whole) ))) fnp
+               uf06 = subst (λ k → odef (filter F)  k) ? fnp
 
 -- this makes check very slow
 -- Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → 
@@ -360,26 +369,26 @@
       →   {x : Ordinal } → odef (filter (Filter-Proj1 {P} {Q} pqa F )) x →  odef (filter F) (& (ZFP (* x) Q))
 FPSet⊆F {P} {Q} {a} pqa F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F uf09 (subst (λ k → odef (filter F) k) (sym &iso) az) uf08 where
       uf08 : * z ⊆ ZFP (* x) Q
-      uf08 = subst (λ k  → * z ⊆ ZFP k Q) (trans (sym *iso) (cong (*) (sym x=ψz))) ZP-proj1⊆ZFP 
+      uf08 = subst (λ k  → * z ⊆ ZFP k Q) ? ZP-proj1⊆ZFP 
       uf09 : Power (ZFP P Q) ∋ ZFP (* x) Q
-      uf09 z xqz with subst (λ k → odef k z) *iso xqz
-      ... | ab-pair {c} {d} xc by = ab-pair uf10  by where
-          uf10 : odef P c
-          uf10 with subst (λ k → odef k c) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) xc
-          ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
+      uf09 z xqz = ? -- with subst (λ k → odef k z) *iso xqz
+      -- ... | ab-pair {c} {d} xc by = ab-pair uf10  by where
+      --    uf10 : odef P c
+      --    uf10 with subst (λ k → odef k c) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) xc
+      --    ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
 
 FQSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
       →   {x : Ordinal } → odef (filter (Filter-Proj2 {P} {Q} pqa F )) x →  odef (filter F) (& (ZFP P (* x) ))
 FQSet⊆F {P} {Q} {a} pqa F {x} record { z = z ; az = az ; x=ψz = x=ψz } = filter1 F uf09 (subst (λ k → odef (filter F) k) (sym &iso) az ) uf08 where
       uf08 : * z ⊆ ZFP P (* x) 
-      uf08 = subst (λ k  → * z ⊆ ZFP P k ) (trans (sym *iso) (cong (*) (sym x=ψz))) ZP-proj2⊆ZFP 
+      uf08 = subst (λ k  → * z ⊆ ZFP P k ) ? ZP-proj2⊆ZFP 
       uf09 : Power (ZFP P Q) ∋ ZFP P (* x) 
-      uf09 z xpz with subst (λ k → odef k z) *iso xpz
-      ... | ab-pair {c} {d} ax yc = ab-pair ax uf10 where
-          uf10 : odef Q d
-          uf10 with subst (λ k → odef k d) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) yc 
-          ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb 
+      uf09 z xpz = ? -- with subst (λ k → odef k z) *iso xpz
+      -- ... | ab-pair {c} {d} ax yc = ab-pair ax uf10 where
+      --     uf10 : odef Q d
+      --     uf10 with subst (λ k → odef k d) (sym (trans (sym *iso) (cong (*) (sym x=ψz)))) yc 
+      --     ... | record { a = a ; aa = aa ; bb = bb ; c∋ab = c∋ab } = bb 
 
 
 -- FQSet⊆F : {P Q a : HOD } → (pqa : ZFP P Q ∋ a ) →