--- a/filter.agda	Sun Jul 05 15:49:00 2020 +0900
+++ b/filter.agda	Sun Jul 05 16:56:21 2020 +0900
@@ -54,7 +54,7 @@
 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
 
 power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
-power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → HODC.double-neg-eilm O (t1 t∋x) } where
+power→⊆ A t  PA∋t = record { incl = λ {x} t∋x → ODC.double-neg-eilm O (t1 t∋x) } where
    t1 : {x : HOD }  → t ∋ x → ¬ ¬ (A ∋ x)
    t1 = zf.IsZF.power→ isZF A t PA∋t
 
@@ -70,6 +70,10 @@
 q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
+open HOD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
 -----
 --
 --  ultra filter is prime
@@ -84,11 +88,11 @@
   lemma3 {p} {q} lt with ultra-filter.ultra u (∪-lemma1 (∈-filter P lt) )
   ... | case1 p∈P  = case1 p∈P
   ... | case2 ¬p∈P = case2 (filter1 P {q ∩ (L ＼ p)} (∪-lemma2 (∈-filter P lt)) lemma7 lemma8) where
-    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) ==  (q ∩ (L ＼ p))
+    lemma5 : ((p ∪ q ) ∩ (L ＼ p)) =h=  (q ∩ (L ＼ p))
     lemma5 = record { eq→ = λ {x} lt → record { proj1 = lemma4 x lt ; proj2 = proj2 lt  }
        ;  eq← = λ {x} lt → record { proj1 = case2 (proj1 lt) ; proj2 = proj2 lt }
       } where
-         lemma4 : (x : Ordinal ) → def ((p ∪ q) ∩ (L ＼ p)) x → def q x
+         lemma4 : (x : Ordinal ) → odef ((p ∪ q) ∩ (L ＼ p)) x → odef q x
          lemma4 x lt with proj1 lt
          lemma4 x lt | case1 px = ⊥-elim ( proj2 (proj2 lt) px )
          lemma4 x lt | case2 qx = qx
@@ -110,11 +114,11 @@
        ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
    } where
         open _==_
-        p+1-p=1 : {p : HOD} → p ⊆ L → L == (p ∪ (L ＼ p)) 
-        eq→ (p+1-p=1 {p} p⊆L) {x} lt with HODC.decp O (def p x)
+        p+1-p=1 : {p : HOD} → p ⊆ L → L =h= (p ∪ (L ＼ p)) 
+        eq→ (p+1-p=1 {p} p⊆L) {x} lt with ODC.decp O (odef p x)
         eq→ (p+1-p=1 {p} p⊆L) {x} lt | yes p∋x = case1 p∋x
         eq→ (p+1-p=1 {p} p⊆L) {x} lt | no ¬p = case2 (record { proj1 = lt ; proj2 = ¬p })
-        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → def L k ) diso (incl p⊆L ( subst (λ k → def p k) (sym diso) p∋x  )) 
+        eq← (p+1-p=1 {p} p⊆L) {x} ( case1 p∋x ) = subst (λ k → odef L k ) diso (incl p⊆L ( subst (λ k → odef p k) (sym diso) p∋x  )) 
         eq← (p+1-p=1 {p} p⊆L) {x} ( case2 ¬p  ) = proj1 ¬p
         lemma : (p : HOD) → p ⊆ L   →  filter P ∋ (p ∪ (L ＼ p))
         lemma p p⊆L = subst (λ k → filter P ∋ k ) (==→o≡ (p+1-p=1 p⊆L)) f∋L