# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1718874917 -32400
# Node ID ca5bfb401ada68ce82564033abea8ff041395663
# Parent  e8c166541c862c17e42395157f36f1b6953ac3b1
...

diff -r e8c166541c86 -r ca5bfb401ada src/LEMC.agda
--- a/src/LEMC.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/LEMC.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -52,11 +52,6 @@
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
-power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
-power→⊆ A t  PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x))  where
-   t1 : {x : HOD }  → t ∋ x → A ∋ x
-   t1 = power→ A t PA∋t
-
 --- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
 ---
 record choiced  ( X : Ordinal ) : Set n where
diff -r e8c166541c86 -r ca5bfb401ada src/NSet.agda
--- a/src/NSet.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/NSet.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --cubical-compatible --safe #-}
+
 open import Level 
 module NSet (n : Level) where
 
diff -r e8c166541c86 -r ca5bfb401ada src/OD.agda
--- a/src/OD.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/OD.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -119,7 +119,7 @@
       eq← = λ {z} d →  eq→  *iso ( eq← eq (eq←  *iso d) )  }
 
 -- =-iso :  {x y : HOD  } → (od x == od y) ≡ (od (* (& x)) == od y)
--- =-iso  {_} {y} = cong ( λ k → od k == od y ) ? -- (sym *iso)
+-- =-iso  {_} {y} = cong ( λ k → od k == od y ) ? -- (==-sym *iso)
 
 ord→== : { x y : HOD  } → & x ≡  & y →  od x == od y
 ord→==  {x} {y} eq = ==-iso (lemma (& x) (& y) (orefl eq)) where
@@ -135,6 +135,9 @@
 *≡*→≡ : { x y : Ordinal  } → * x ≡ * y →  x ≡ y
 *≡*→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) eq )
 
+&≡&*& : {x : HOD} → & x ≡ & (* (& x))
+&≡&*& = (==→o≡ (==-sym *iso) )
+
 --- &≡&→≡ : { x y : HOD  } → & x ≡  & y →  x ≡ y
 --  &≡&→≡ eq = ? -- subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) eq )
 
@@ -302,9 +305,6 @@
 ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
 ψiso {ψ} t refl = t
 
-*iso== : {y : HOD} → od y == od (* (& y))
-*iso== {y} = record { eq→ = λ {x} yx → eq← *iso yx ; eq← = λ {x} yx → eq→ *iso yx }
-
 record RCod (COD : HOD) (ψ : HOD → HOD)  : Set (suc n) where
  field
      ≤COD : ∀ {x : HOD } → ψ x ⊆ COD 
@@ -325,7 +325,7 @@
             r01 = sym (Replaced.x=ψz lt )
 
 replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → {C : HOD} → (rc : RCod C ψ) → Replace X ψ rc ∋ ψ x
-replacement← {ψ} X x lt {C} rc = record { z = & x ; az = lt  ; x=ψz = ==→o≡ (RCod.ψ-eq rc *iso== ) }
+replacement← {ψ} X x lt {C} rc = record { z = & x ; az = lt  ; x=ψz = ==→o≡ (RCod.ψ-eq rc (==-sym *iso) ) }
 replacement→ : {ψ : HOD → HOD} (X x : HOD) → {C : HOD} → (rc : RCod C ψ ) → (lt : Replace X ψ rc ∋ x) 
    →  ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 replacement→ {ψ} X x {C} rc lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) 
@@ -488,22 +488,22 @@
       lemma4 : owner ≡ & (x , x) 
       lemma4 = trans ao ( ==→o≡ record { eq→ = lemma5 _ ; eq← = lemma6 _ } ) where
           lemma5 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x)
-          lemma5 y (case1 eq) = case1 (trans eq (sym (==→o≡ *iso== ) ))
-          lemma5 y (case2 eq) = case1 (trans eq (sym (==→o≡ *iso== ) ))
+          lemma5 y (case1 eq) = case1 (trans eq (sym (==→o≡ (==-sym *iso) ) ))
+          lemma5 y (case2 eq) = case1 (trans eq (sym (==→o≡ (==-sym *iso) ) ))
           lemma6 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) 
-          lemma6 y (case1 eq) = case1 (trans eq ((==→o≡ *iso== ) ))
-          lemma6 y (case2 eq) = case1 (trans eq ((==→o≡ *iso== ) ))
+          lemma6 y (case1 eq) = case1 (trans eq ((==→o≡ (==-sym *iso) ) ))
+          lemma6 y (case2 eq) = case1 (trans eq ((==→o≡ (==-sym *iso) ) ))
   lemma3 :  {y : Ordinal}  → Own (x , (x , x)) y → Own (* (& x) , (* (& x) , * (& x))) y
   lemma3 {y} record { owner = owner ; ao = (case1 ao) ; ox = ox } = record { owner = owner 
-        ; ao = case1 (trans ao (==→o≡ *iso== )) ; ox = ox }
+        ; ao = case1 (trans ao (==→o≡ (==-sym *iso) )) ; ox = ox }
   lemma3 {y} record { owner = owner ; ao = (case2 ao) ; ox = ox } = record { owner = owner 
         ; ao = case2 (trans ao (==→o≡ record { eq→ = lemma5 _ ; eq← = lemma4 _  }))  ; ox = ox } where
        lemma4 : (x₁ : Ordinal) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x))) → (x₁ ≡ & x) ∨ (x₁ ≡ & x)
-       lemma4 y (case1 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) ))
-       lemma4 y (case2 eq) = case1 ( trans eq (sym (==→o≡ *iso== ) ))
+       lemma4 y (case1 eq) = case1 ( trans eq (sym (==→o≡ (==-sym *iso) ) ))
+       lemma4 y (case2 eq) = case1 ( trans eq (sym (==→o≡ (==-sym *iso) ) ))
        lemma5 : (x₁ : Ordinal) → (x₁ ≡ & x) ∨ (x₁ ≡ & x) → (x₁ ≡ & (* (& x))) ∨ (x₁ ≡ & (* (& x)))
-       lemma5 y (case1 eq) = case1 ( trans eq ((==→o≡ *iso== ) ))
-       lemma5 y (case2 eq) = case1 ( trans eq ((==→o≡ *iso== ) ))
+       lemma5 y (case1 eq) = case1 ( trans eq ((==→o≡ (==-sym *iso) ) ))
+       lemma5 y (case2 eq) = case1 ( trans eq ((==→o≡ (==-sym *iso) ) ))
 
 infinity : (ho< : ODAxiom-ho<) → (x : HOD) → Omega ho< ∋ x → Omega ho< ∋ Union (x , (x , x ))
 infinity ho< x lt = subst (λ k → odef (Omega ho<) k ) (==→o≡ Omega-iso) (isuc {& x} lt) 
@@ -519,11 +519,11 @@
 pair-iso : {x y : HOD } →  (* (& x) , * (& y)) =h= (x , y)
 pair-iso {x} {y} = record { eq→ = lem01 ; eq← = lem00  } where
   lem00 :  {z : Ordinal} →  (z ≡ & x) ∨ (z ≡ & y) → (z ≡ & (* (& x))) ∨ (z ≡ & (* (& y)))
-  lem00 {z} (case1 z=x) = case1 (trans z=x ((==→o≡ *iso== ) ))
-  lem00 {z} (case2 z=y) = case2 (trans z=y ((==→o≡ *iso== ) ))
+  lem00 {z} (case1 z=x) = case1 (trans z=x ((==→o≡ (==-sym *iso) ) ))
+  lem00 {z} (case2 z=y) = case2 (trans z=y ((==→o≡ (==-sym *iso) ) ))
   lem01 :  {z : Ordinal}  → (z ≡ & (* (& x))) ∨ (z ≡ & (* (& y))) →  (z ≡ & x) ∨ (z ≡ & y)
-  lem01 {z} (case1 z=x) = case1 (trans z=x (sym (==→o≡ *iso== ) ))
-  lem01 {z} (case2 z=y) = case2 (trans z=y (sym (==→o≡ *iso== ) ))
+  lem01 {z} (case1 z=x) = case1 (trans z=x (sym (==→o≡ (==-sym *iso) ) ))
+  lem01 {z} (case2 z=y) = case2 (trans z=y (sym (==→o≡ (==-sym *iso) ) ))
 
 o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y)
 o<→c< lt {z} ox = ordtrans ox lt
@@ -542,8 +542,8 @@
 
 selection : {ψ : HOD → Set n} → { zψ : ZPred HOD _∋_ _=h=_ ψ } → { X y : HOD} →   ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ zψ ∋ y)
 selection {ψ} {zψ} {X} {y}   = ⟪
-     ( λ cond → ⟪ proj1 cond , peq  (proj2 cond) *iso==  ⟫ )
-  ,  ( λ select → ⟪ proj1 select  , peq (proj2 select) (==-sym *iso== )  ⟫ )
+     ( λ cond → ⟪ proj1 cond , peq  (proj2 cond) (==-sym *iso)  ⟫ )
+  ,  ( λ select → ⟪ proj1 select  , peq (proj2 select) *iso  ⟫ )
   ⟫ where
      peq : {x y : HOD } →  ψ x →  od x == od y  → ψ y
      peq {x} {y} fx eq = proj1 (ZPred.ψ-cong zψ x y eq) fx
@@ -580,7 +580,7 @@
             r01 = sym (Replaced.x=ψz lt )
 
 zf-replacement← :  {ψ : HOD → HOD} → {zfψ :  ZFunc HOD _∋_ _=h=_ ψ } → (X x : HOD) →  X ∋ x → ZFReplace X ψ zfψ ∋ ψ x
-zf-replacement← {ψ} {zfψ} X x lt = record { z = & x ; az = lt  ; x=ψz = ==→o≡  (ZFunc.ψ-cong zfψ _ _ *iso==  ) }
+zf-replacement← {ψ} {zfψ} X x lt = record { z = & x ; az = lt  ; x=ψz = ==→o≡  (ZFunc.ψ-cong zfψ _ _ (==-sym *iso)  ) }
 zf-replacement→ : {ψ : HOD → HOD} → {zfψ : ZFunc HOD _∋_ _=h=_ ψ } → (X x : HOD) 
      → (lt : ZFReplace X ψ zfψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
 zf-replacement→ {ψ} {zfψ} X x lt eq = eq (* (Replaced.z lt)) (ord→== (Replaced.x=ψz lt)) 
diff -r e8c166541c86 -r ca5bfb401ada src/ODC.agda
--- a/src/ODC.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/ODC.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -63,7 +63,7 @@
    lemma eq p0 = ¬x<0  {& ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
    ¬p : (& ps ≡ o∅) → p → ⊥
    ¬p eq =  lemma ( begin
-      pred-od p  ≈⟨ *iso== ⟩
+      pred-od p  ≈⟨ ==-sym  *iso ⟩
       * ( & ps ) ≡⟨ cong (*) eq ⟩
       * ( o∅ ) ≈⟨ o∅==od∅ ⟩
       od∅ ∎ ) where open EqR ==-Setoid
@@ -101,14 +101,6 @@
 ... | case1 a = case1 a
 ... | case2 ¬a = case2 ( ab ¬a)
 
-power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
-power→⊆ A t  PA∋t tx = subst (λ k → odef A k ) &iso ( power→ A t PA∋t (subst (λ k → odef t k) (sym &iso) tx ) )
-
-power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
-power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01  where
-   p01 :  {z : HOD} → (x ∩ y) ∋ z → A ∋ z
-   p01 {z} xyz = power→ A x ax (proj1 xyz )
-
 OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
 OrdP  x y with trio< x (& y)
 OrdP  x y | tri< a ¬b ¬c = no ¬c
diff -r e8c166541c86 -r ca5bfb401ada src/ODUtil.agda
--- a/src/ODUtil.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/ODUtil.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -50,6 +50,17 @@
 ⊆∩-incl-2 : {a b c : HOD} → a ⊆ c → ( b ∩ a ) ⊆ c
 ⊆∩-incl-2 {a} {b} {c} a<c {z} ab = a<c (proj2 ab)
 
+power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
+power→⊆ A t  PA∋t t∋x = subst (λ k → odef A k ) &iso ( t1 (subst (λ k → odef t k ) (sym &iso) t∋x))  where
+   t1 : {x : HOD }  → t ∋ x → A ∋ x
+   t1 = power→ A t PA∋t
+
+power-∩ : { A x y : HOD } → Power A ∋ x → Power A ∋ y → Power A ∋ ( x ∩ y )
+power-∩ {A} {x} {y} ax ay = power← A (x ∩ y) p01  where
+   p01 :  {z : HOD} → (x ∩ y) ∋ z → A ∋ z
+   p01 {z} xyz = power→ A x ax (proj1 xyz )
+
+
 cseq :  HOD  →  HOD
 cseq x = record { od = record { def = λ y → odef x (osuc y) } ; odmax = osuc (odmax x) ; <odmax = lemma } where
     lemma : {y : Ordinal} → def (od x) (osuc y) → y o< osuc (odmax x)
@@ -148,7 +159,7 @@
 
 ω-prev-eq1 : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → ¬ (x o< y)
 ω-prev-eq1 {x} {y} eq x<y with  eq→ (ord→== eq) record { owner = & (* y , * y) ; ao = case2 refl
-        ; ox = eq→ *iso== (case1 refl) }   --  (* x , (* x , * x)) ∋ * y
+        ; ox = eq→ (==-sym *iso) (case1 refl) }   --  (* x , (* x , * x)) ∋ * y
 ... | record { owner = u ; ao = xxx∋u ; ox = uy } with xxx∋u
 ... | case1 u=x = ⊥-elim ( o<> x<y (osucprev (begin
        osuc y ≡⟨ sym (cong osuc  &iso) ⟩
@@ -158,7 +169,7 @@
        & (* x) ≡⟨ &iso ⟩
        x ∎ ))) where open o≤-Reasoning O
 ... | case2 u=xx = ⊥-elim (o<¬≡ ( begin
-        x ≡⟨ single& ( eq← *iso==  (subst₂ (λ j k → odef j k ) (cong (*) u=xx ) &iso uy)) ⟩
+        x ≡⟨ single& ( eq← (==-sym *iso)  (subst₂ (λ j k → odef j k ) (cong (*) u=xx ) &iso uy)) ⟩
         y ∎ ) x<y)  where open ≡-Reasoning
 
 Omega-inject : {x y : Ordinal} →  & (Union (* y , (* y , * y))) ≡ & (Union (* x , (* x , * x))) → y ≡ x
@@ -171,7 +182,7 @@
 ω-inject {x} {y} eq = ord→== ( Omega-inject (==→o≡ (==-trans Omega-iso (==-trans eq (==-sym Omega-iso)))))
 
 ω-∈s : (x : HOD) →  Union ( x , (x , x)) ∋ x
-ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl  ; ox = eq→ *iso== (case2 refl) }
+ω-∈s x = record { owner = & ( x , x ) ; ao = case2 refl  ; ox = eq→ (==-sym *iso) (case2 refl) }
 
 ωs≠0 : (x : HOD) →  ¬ ( Union ( x , (x , x)) =h= od∅ )
 ωs≠0 x =  ∅< {Union ( x , ( x ,  x))} (ω-∈s  _)
@@ -193,12 +204,12 @@
     Union (y , (y , y)) ∎ where open EqR ==-Setoid                       
 
 nat→ω-iso : {i : HOD} → (lt : Omega ho< ∋ i ) → nat→ω ( ω→nat i lt ) =h= i
-nat→ω-iso {i} lt = ==-trans (nat→ω-iso-ord _ lt) (==-sym *iso==) where
+nat→ω-iso {i} lt = ==-trans (nat→ω-iso-ord _ lt) *iso where
     nat→ω-iso-ord : (x : Ordinal) → (lt : odef (Omega ho< ) x) → nat→ω ( ω→nato lt ) =h= (* x)
     nat→ω-iso-ord _ OD.iφ = ==-sym o∅==od∅
-    nat→ω-iso-ord x (OD.isuc OD.iφ) = ==-trans (Omega-subst _ _ (==-sym o∅==od∅)) *iso==
+    nat→ω-iso-ord x (OD.isuc OD.iφ) = ==-trans (Omega-subst _ _ (==-sym o∅==od∅)) (==-sym *iso)
     nat→ω-iso-ord x (OD.isuc (OD.isuc {y} lt)) = ==-trans (Omega-subst _ _ 
-      (==-trans (Omega-subst _ _ lem02 ) *iso==) ) *iso==  where
+      (==-trans (Omega-subst _ _ lem02 ) (==-sym *iso)))  (==-sym *iso)  where
       lem02  : nat→ω ( ω→nato lt ) =h= (* y)
       lem02  = nat→ω-iso-ord y lt
 
@@ -208,20 +219,20 @@
     Union (nat→ω x , (nat→ω x , nat→ω x)) ≈⟨ ==-sym eq ⟩
     * o∅ ≈⟨ o∅==od∅  ⟩
     od∅ ∎ )) where open EqR ==-Setoid
-ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (==-trans *iso== eq) )
+ω→nat-iso0 Zero (isuc ltd) eq = ⊥-elim ( ωs≠0 _ (==-trans (==-sym *iso) eq) )
 ω→nat-iso0 (Suc i) (isuc {x} ltd) eq = cong Suc ( ω→nat-iso0 i ltd (lemma1 eq) ) where
        lemma1 :  * (& (Union (* x , (* x , * x)))) =h= Union (nat→ω i , (nat→ω i , nat→ω i)) → * x =h= nat→ω i
        lemma1 eq = begin
           * x  ≈⟨ (o≡→== ( Omega-inject  (==→o≡ (begin
-             Union (* x , (* x , * x)) ≈⟨  *iso== ⟩
+             Union (* x , (* x , * x)) ≈⟨ ==-sym  *iso ⟩
              * (& ( Union (* x , (* x , * x)))) ≈⟨  eq ⟩
              Union ((nat→ω i) , (nat→ω i , nat→ω i)) ≈⟨ ==-sym Omega-iso ⟩
              Union (* (& (nat→ω i)) , (* (& (nat→ω i)) , * (& (nat→ω i)))) ∎ )) ))  ⟩
-          * (& ( nat→ω i))  ≈⟨ (==-sym *iso==)  ⟩
+          * (& ( nat→ω i))  ≈⟨ *iso ⟩
           nat→ω i ∎  where open EqR ==-Setoid
 
 ω→nat-iso : {i : Nat} → ω→nat ( nat→ω i ) (ω∋nat→ω {i}) ≡ i
-ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) (==-sym *iso==)
+ω→nat-iso {i} = ω→nat-iso0 i (ω∋nat→ω {i}) *iso
 
 nat→ω-inject : {i j : Nat} → nat→ω i =h=  nat→ω j → i ≡ j
 nat→ω-inject {Zero} {Zero} eq = refl
@@ -238,7 +249,7 @@
          ; x=ψz = trans  x=ψz (cong (&) (eq az) ) }
 
 PPP : {P : HOD} → Power P ∋ P
-PPP {P} z pz = eq← *iso== pz
+PPP {P} z pz = eq← (==-sym *iso) pz
 
 UPower⊆Q : {P Q : HOD} → P ⊆ Q → Union (Power P) ⊆ Q
 UPower⊆Q {P} {Q} P⊆Q {z} record { owner = y ; ao = ppy ; ox = yz } = P⊆Q (ppy _ yz)
@@ -248,5 +259,5 @@
 UPower∩ {P} each {p} {q} record { owner = x ; ao = ppx ; ox = xz } record { owner = y ; ao = ppy ; ox = yz }
    =  record { owner = & P ; ao = PPP ; ox = lem03 }  where
     lem03 :   odef (* (& P)) (& (p ∩ q))
-    lem03 = eq→  *iso== ( each (ppx _ xz) (ppy _ yz) )
+    lem03 = eq→  (==-sym *iso) ( each (ppx _ xz) (ppy _ yz) )
 
diff -r e8c166541c86 -r ca5bfb401ada src/OrdUtil.agda
--- a/src/OrdUtil.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/OrdUtil.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -255,84 +255,9 @@
   → ¬ p
 FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
 
--- nexto∅ : {x : Ordinal} → o∅ o< next x
--- nexto∅ {x} with trio< o∅ x
--- nexto∅ {x} | tri< a ¬b ¬c = ordtrans a x<nx
--- nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
--- nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
-
--- next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
--- next< {x} {y} {z} x<nz y<nx with trio< y (next z)
--- next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
--- next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
---    (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
--- next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
---    (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
-
 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
 osuc< {x} {y} refl = <-osuc
 
--- nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y
--- nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
-
--- nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
--- nexto≡ {x} with trio< (next x) (next (osuc x) )
---    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
--- nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
---    (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
--- nexto≡ {x} | tri≈ ¬a b ¬c = b
---    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
--- nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
---    (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
-
--- next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
--- next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
---     y<nx : y o< next x
---     y<nx = osuc< (sym eq)
-
--- omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
--- omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
-
--- x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
--- x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)
--- x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
---      ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
--- x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
--- x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
---      ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
-
--- ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
--- ≤next {x} {y} x≤y with trio< (next x) y
--- ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
--- ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
--- ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
--- ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x
--- ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x
-
--- x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
--- x<ny→≤next {x} {y} x<ny with trio< x y
--- x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
--- x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl
--- x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny ))
-
--- omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
--- omax<nomax {x} {y} with trio< x y
--- omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
--- omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
--- omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
-
--- omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
--- omax<nx {x} {y} {z} x<nz y<nz with trio< x y
--- omax<nx {x} {y} {z} x<nz y<nz | tri< a ¬b ¬c = osuc<nx y<nz
--- omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
--- omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
-
--- nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
--- nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
--- nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
--- nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
--- nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
-
 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
   field
     os→ : (x : Ordinal) → x o< maxordinal → Ordinal
diff -r e8c166541c86 -r ca5bfb401ada src/filter.agda
--- a/src/filter.agda	Tue Jun 18 18:46:53 2024 +0900
+++ b/src/filter.agda	Thu Jun 20 18:15:17 2024 +0900
@@ -1,41 +1,50 @@
-{-# 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 {n : Level } (O : Ordinals {n})   where
+import HODBase
+import OD
+open import Relation.Nullary
+module filter {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
-import OD 
-
-open import Relation.Nullary 
-open import Data.Empty 
-open import Relation.Binary.Core
-open import Relation.Binary.PropositionalEquality
-import BAlgebra 
-
-open BAlgebra O
+open import nat
 
-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
-
-
-import ODC
-open ODC O
+open ODUtil O HODAxiom  ho<
 
 open _∧_
 open _∨_
 open Bool
 
+open  HODBase._==_
+
+open HODBase.ODAxiom HODAxiom  
+open OD O HODAxiom
+
+open HODBase.HOD
+
+open AxiomOfChoice AC
+open import ODC O HODAxiom AC as ODC
+
+-- import BAlgebra 
+-- open BAlgebra O
+-- 
 -- L is a boolean algebra, but we don't assume this explicitly
 --
 --     NEG : {p : HOD} → L ∋ p → L ∋ (P ＼ p)
@@ -76,21 +85,20 @@
 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
 q∩q⊆q lt = proj1 lt 
 
-∩→≡1 : {p q : HOD } → p ⊆ q → (q ∩ p) ≡ p
-∩→≡1 {p} {q} p⊆q =  ==→o≡ record { eq→ = c00 ; eq← = c01 } where
+∩→≡1 : {p q : HOD } → p ⊆ q → (q ∩ p) =h= p
+∩→≡1 {p} {q} p⊆q =  record { eq→ = c00 ; eq← = c01 } where
     c00 : {x : Ordinal} → odef (q ∩ p) x → odef p x
     c00 {x} qpx = proj2 qpx
     c01 : {x : Ordinal} → odef p x → odef (q ∩ p) x 
     c01 {x} px = ⟪ p⊆q px , px  ⟫
 
-∩→≡2 : {p q : HOD } → q ⊆ p → (q ∩ p) ≡ q
-∩→≡2 {p} {q} q⊆p =  ==→o≡ record { eq→ = c00 ; eq← = c01 } where
+∩→≡2 : {p q : HOD } → q ⊆ p → (q ∩ p) =h= q
+∩→≡2 {p} {q} q⊆p =  record { eq→ = c00 ; eq← = c01 } where
     c00 : {x : Ordinal} → odef (q ∩ p) x → odef q x
     c00 {x} qpx = proj1 qpx
     c01 : {x : Ordinal} → odef q x → odef (q ∩ p) x 
     c01 {x} qx = ⟪ qx , q⊆p qx  ⟫
 
-open HOD
 
 -----
 --
@@ -118,11 +126,11 @@
          lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
          lemma4 x lt | case2 qx = qx
     lemma9 : L ∋ ((p ∪ q ) ∩ (P ＼ p))
-    lemma9 = subst (λ k → L ∋ k ) (sym (==→o≡ lemma5)) (CAP Lq (NEG Lp))
+    lemma9 = subst (λ k → odef L k ) (sym (==→o≡ lemma5)) (CAP Lq (NEG Lp))
     lemma6 : filter F ∋ ((p ∪ q ) ∩ (P ＼ p))
     lemma6 = filter2 F lt ¬p∈P  lemma9
     lemma7 : filter F ∋ (q ∩ (P ＼ p))
-    lemma7 =  subst (λ k → filter F ∋ k ) (==→o≡ lemma5 ) lemma6
+    lemma7 =  subst (λ k → odef (filter F)  k ) (==→o≡ lemma5 ) lemma6
     lemma8 : (q ∩ (P ＼ p)) ⊆ q
     lemma8 lt = proj1 lt
 
@@ -131,6 +139,13 @@
 --  if Filter {L} {P} contains L, prime filter is ultra
 --
 
+U-F=∅→F⊆U : {L F U : HOD} → U ⊆ L  →  ((x : Ordinal) →  ¬ ( odef F x ∧ ( ¬ odef U x ))) → F ⊆ U
+U-F=∅→F⊆U {L} {F} {U} U⊆L not = gt02  where
+    gt02 : { x : Ordinal } → odef F x → odef U x
+    gt02 {x} fx with ODC.∋-p U (* x)
+    ... | yes y = subst (λ k → odef U k ) &iso y
+    ... | no  n = ⊥-elim ( not x ⟪ fx , subst (λ k → ¬ odef U k ) &iso n ⟫ )
+
 filter-lemma2 :  {P L : HOD} → (LP : L ⊆ Power P)
        → ({p : HOD} → L ∋ p → L ∋ ( P ＼ p))
        → (F : Filter {L} {P} LP)  → filter F ∋ P → prime-filter F → ultra-filter F
@@ -138,17 +153,16 @@
          proper = prime-filter.proper prime
        ; ultra = λ {p}  L∋p _ → prime-filter.prime prime L∋p (NEG  L∋p) (lemma p (p⊆L  L∋p ))  
    } where
-        open _==_
         p⊆L : {p : HOD} → L ∋ p  → p ⊆ P
         p⊆L {p} lt = power→⊆ P p ( LP lt )
         p+1-p=1 : {p : HOD} → p ⊆ P  → P =h= (p ∪ (P ＼ p)) 
-        eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp O (odef p x)
+        eq→ (p+1-p=1 {p} p⊆P) {x} lt with ODC.decp (odef p x)
         eq→ (p+1-p=1 {p} p⊆P) {x} lt | yes p∋x = case1 p∋x
         eq→ (p+1-p=1 {p} p⊆P) {x} lt | no ¬p = case2 ⟪ lt , ¬p ⟫
         eq← (p+1-p=1 {p} p⊆P) {x} ( case1 p∋x ) = subst (λ k → odef P k ) &iso (p⊆P ( subst (λ k → odef p k) (sym &iso) p∋x  )) 
         eq← (p+1-p=1 {p} p⊆P) {x} ( case2 ¬p  ) = proj1 ¬p
         lemma : (p : HOD) → p ⊆ P   →  filter F ∋ (p ∪ (P ＼ p))
-        lemma p p⊆P = subst (λ k → filter F ∋ k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P 
+        lemma p p⊆P = subst (λ k → odef (filter F ) k ) (==→o≡ (p+1-p=1 {p} p⊆P)) f∋P 
 
 record Ideal   {L P : HOD } (LP : L ⊆ Power P) : Set (suc n) where
    field
@@ -188,18 +202,18 @@
 max→ultra {L} {P} LP CAP F0 {y} mfy mx = record { proper = MaximumFilter.proper mx ; ultra = ultra } where
     mf = MaximumFilter.mf mx
     ultra : {p : HOD} → L ∋ p → L ∋ (P ＼ p) → (filter mf ∋ p) ∨ (filter mf ∋ (P ＼ p))
-    ultra {p} Lp Lnp with ODC.∋-p O (filter mf) p 
+    ultra {p} Lp Lnp with ODC.∋-p (filter mf) p 
     ... | yes y = case1 y
-    ... | no np = case2 (subst (λ k → k ∋ (P ＼ p)) F=mf F∋P-p) where
+    ... | no np = case2 (eq→ F=mf F∋P-p ) where  
          F : HOD  
          F = record { od = record { def = λ x →  odef L x ∧ Fp {L} {P} LP F0 mx (& p) x } 
             ; odmax = & L ; <odmax = λ lt → odef< (proj1 lt) } 
          mu01 :  {r : HOD} {q : HOD} → L ∋ q → F ∋ r → r ⊆ q → F ∋ q
          mu01 {r} {q} Lq ⟪ Lr , record { y = y ; mfy = mfy ; y-p⊂x = y-p⊂x } ⟫ r⊆q = ⟪ Lq , record { y = y ; mfy = mfy ; y-p⊂x = mu03 } ⟫ where
             mu05 : (* y ＼ p) ⊆ r
-            mu05 = subst₂ (λ j k → (* y ＼ j ) ⊆ k ) *iso *iso y-p⊂x
+            mu05 ⟪ yx , ¬px ⟫  =  eq→  *iso (y-p⊂x ⟪ yx , (λ np → ¬px (eq→  *iso np ) ) ⟫ ) 
             mu04 :  (* y ＼ * (& p)) ⊆ * (& q)
-            mu04 {x} ⟪ yx , npx ⟫ = subst (λ k → odef k x ) (sym *iso) (r⊆q (mu05 ⟪ yx , (λ px1 → npx (subst (λ k → odef k x) (sym *iso) px1 )) ⟫ )  )
+            mu04 {x} ⟪ yx , npx ⟫ = eq← *iso (r⊆q (mu05 ⟪ yx , (λ px1 → npx (eq← *iso px1 )) ⟫ ) )
             mu03 :  (* y ＼ * (& p)) ⊆ * (& q)
             mu03 = mu04 
          mu02 : {r : HOD} {q : HOD} → F ∋ r → F ∋ q → L ∋ (r ∩ q) → F ∋ (r ∩ q)
@@ -210,12 +224,9 @@
             mu20 : odef (filter mf) (& (* qy ∩ * ry))
             mu20 = filter2 mf (subst (λ k → odef (filter mf) k) (sym &iso) mfqy) (subst (λ k → odef (filter mf) k) (sym &iso) mfry)  mu21
             mu24 : ((* qy ∩ * ry) ＼ * (& p)) ⊆ (r ∩ q)
-            mu24 {x} ⟪ qry , npx ⟫ = ⟪ subst (λ k → odef k x) *iso ( ry-p⊂x ⟪ proj2 qry , npx ⟫ )  
-               , subst (λ k → odef k x) *iso ( qy-p⊂x ⟪ proj1 qry , npx ⟫ )   ⟫
-            mu23 : ((* qy ∩ * ry) ＼ * (& p) ) ⊆ (r ∩ q)
-            mu23 = mu24 
+            mu24 {x} ⟪ qry , npx ⟫ = ⟪ eq→ *iso ( ry-p⊂x ⟪ proj2 qry , npx ⟫ ) , eq→ *iso ( qy-p⊂x ⟪ proj1 qry , npx ⟫ ) ⟫
             mu22 : (* (& (* qy ∩ * ry)) ＼ * (& p)) ⊆ * (& (r ∩ q))
-            mu22 = subst₂ (λ j k → (j ＼ * (& p)) ⊆ k ) (sym *iso) (sym *iso) mu23
+            mu22 {x} ⟪ qry , px ⟫ = eq← *iso ( mu24 ⟪ eq→ *iso qry  , px ⟫ )
          FisFilter : Filter {L} {P} LP
          FisFilter = record { filter = F ; f⊆L = λ {x} lt → proj1 lt  ; filter1 = mu01 ; filter2 = mu02 }
          FisGreater : {x : Ordinal } → odef (filter (MaximumFilter.mf mx))  x → odef (filter FisFilter ) x
@@ -227,26 +238,25 @@
              mxy : odef (filter (MaximumFilter.mf mx)) y
              mxy = MaximumFilter.F⊆mf mx mfy
              mu30 : (* y ＼ * (& p)) ⊆ * (& (P ＼ p))
-             mu30 {z} ⟪ yz , ¬pz ⟫ = subst (λ k → odef k z) (sym *iso) ( ⟪ Pz , (λ pz → ¬pz (subst (λ k → odef k z) (sym *iso) pz ))  ⟫  ) where
+             mu30 {z} ⟪ yz , ¬pz ⟫ = eq← *iso ⟪ Pz , ( λ pz → ¬pz ( eq← *iso pz ))  ⟫  where
                  Pz : odef P z
                  Pz = LP (f⊆L mf mxy ) _ yz
          FisProper : ¬ (filter FisFilter ∋ od∅)    -- if F contains p, p is in mf which contract np
          FisProper ⟪ L0 , record { y = z ; mfy = mfz ; y-p⊂x = z-p⊂x } ⟫ = 
            ⊥-elim ( np (filter1 mf Lp (subst (λ k → odef (filter mf) k) (sym &iso) mfz) mu31) ) where
              mu31 : * z ⊆ p
-             mu31 {x} zx with ODC.decp O (odef p x)
+             mu31 {x} zx with ODC.decp (odef p x)
              ... | yes px = px
-             ... | no npx = ⊥-elim ( ¬x<0 (subst (λ k → odef k x) *iso (z-p⊂x ⟪ zx , (λ px → npx (subst (λ k → odef k x) *iso px) ) ⟫ ) ) )
+             ... | no npx = ⊥-elim ( ¬x<0 ( eq→  *iso (z-p⊂x ⟪ zx , (λ px → npx ( eq→  *iso px) ) ⟫ ) ) )
          F0⊆F : filter F0 ⊆ F
          F0⊆F {x} fx = ⟪ f⊆L F0 fx , record { y = _ ; mfy = MaximumFilter.F⊆mf mx fx ; y-p⊂x = mu42 } ⟫ where
              mu42 : (* x ＼ * (& p)) ⊆ * x
              mu42 {z} ⟪ xz , ¬p ⟫ = xz
-         F=mf : F ≡ filter mf
+         F=mf : F =h= filter mf
          F=mf with osuc-≡< ( ⊆→o≤ FisGreater )
-         ... | case1 eq = &≡&→≡ (sym eq)
+         ... | case1 eq = ord→== (sym eq) -- &≡&→≡ (sym eq)
          ... | case2 lt = ⊥-elim ( MaximumFilter.is-maximum mx FisFilter FisProper F0⊆F ⟪ lt , FisGreater ⟫ )
 
-open _==_
 
 ultra→max : {L P : HOD} (LP : L ⊆ Power P) → ({p : HOD} 
        → L ∋ p → L ∋ ( P ＼ p)) 
@@ -260,19 +270,19 @@
          um02 : {y : Ordinal } → odef (filter F) y ∧ (¬ odef (filter U) y) → y o< & L
          um02 {y} Fy = odef< ( f⊆L F (proj1 Fy ) )
      GT≠∅ :  ¬ (GT =h= od∅)
-     GT≠∅ eq = ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where
-         U≠F : ¬ ( filter U ≡ filter F )
-         U≠F eq = o<¬≡ (cong (&) eq) U<F
-         gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x))
-         gt01 x not = ¬x<0 ( eq→ eq not )
+     GT≠∅ eq = ? where -- ⊥-elim (U≠F ( ==→o≡ ((⊆→= {filter U} {filter F}) U⊆F (U-F=∅→F⊆U {filter F} {filter U} gt01)))) where
+        U≠F : ¬ ( filter U ≡ filter F )
+        U≠F eq = o<¬≡ (cong (&) eq) U<F
+        gt01 : (x : Ordinal) → ¬ ( odef (filter F) x ∧ (¬ odef (filter U) x))
+        gt01 x not = ¬x<0 ( eq→ eq not )
      p : HOD
-     p = ODC.minimal O GT GT≠∅
+     p = minimal GT GT≠∅
      ¬U∋p : ¬ ( filter U ∋ p )
-     ¬U∋p = proj2 (ODC.x∋minimal O GT GT≠∅)
+     ¬U∋p = ? -- proj2 (ODC.x∋minimal O GT GT≠∅)
      L∋p : L ∋  p
-     L∋p = f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅))
+     L∋p = ? -- f⊆L F ( proj1 (ODC.x∋minimal O GT GT≠∅))
      um00 : ¬ odef (filter U) (& p)
-     um00 = proj2 (ODC.x∋minimal O GT GT≠∅)
+     um00 = ? -- proj2 (ODC.x∋minimal O GT GT≠∅)
      L∋-p : L ∋  ( P ＼ p )
      L∋-p = NEG L∋p
      U∋-p : filter U ∋  ( P ＼ p )
@@ -280,11 +290,11 @@
      ... | case1 ux = ⊥-elim ( ¬U∋p ux )
      ... | case2 u-x = u-x
      F∋p : filter F ∋ p
-     F∋p = proj1 (ODC.x∋minimal O GT GT≠∅)
+     F∋p = ? -- proj1 (ODC.x∋minimal O GT GT≠∅)
      F∋-p : filter F ∋ ( P ＼ p )
      F∋-p = U⊆F U∋-p 
      f0 : filter F ∋ od∅
-     f0 = subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) )
+     f0 = ? -- subst (λ k → odef (filter F) k ) (trans (cong (&) ∩-comm) (cong (&) [a-b]∩b=0 ) ) ( filter2 F F∋p F∋-p ( CAP L∋p L∋-p) )
 
 --  if there is a filter , there is a ultra filter under the axiom of choise
 --        Zorn Lemma
@@ -298,10 +308,10 @@
 
 Filter-is-Filter : { L P : HOD  } (LP : L ⊆ Power P) → (F : Filter {L} {P} LP) → (proper : ¬ (filter F) ∋ od∅ ) → IsFilter {L} {P} LP (& (filter F))
 Filter-is-Filter {L} {P} LP F proper = record { 
-       f⊆L     = subst (λ k → k ⊆ L ) (sym *iso) (f⊆L F)
-     ; filter1 = λ {p} {q} Lq Fp p⊆q → subst₂ (λ j k → odef j k ) (sym *iso) &iso 
-        ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q  )
-     ; filter2 = λ {p} {q} Fp Fq Lpq → subst₂ (λ j k → odef j k ) (sym *iso) refl ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp)
-         (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq )
-     ; proper  = subst₂ (λ j k → ¬ odef j k ) (sym *iso) ord-od∅ proper 
+       f⊆L     = ? -- subst (λ k → k ⊆ L ) (sym *iso) (f⊆L F)
+     ; filter1 = ? -- λ {p} {q} Lq Fp p⊆q → subst₂ (λ j k → odef j k ) (sym *iso) &iso 
+        -- ( filter1 F (subst (λ k → odef L k) (sym &iso) Lq) (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp) p⊆q  )
+     ; filter2 = ? -- λ {p} {q} Fp Fq Lpq → subst₂ (λ j k → odef j k ) (sym *iso) refl ( filter2 F (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fp)
+         -- (subst₂ (λ j k → odef j k ) *iso (sym &iso) Fq) Lpq )
+     ; proper  = ? -- subst₂ (λ j k → ¬ odef j k ) (sym *iso) ord-od∅ proper 
    }