# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1595042978 -32400
# Node ID 7f919d6b045b73bc9ef4013d80f45c05f53e020b
# Parent  67580311cc8e90a0178d7f47d67c1a1408b4fd46
...

diff -r 67580311cc8e -r 7f919d6b045b LEMC.agda
--- a/LEMC.agda	Sat Jul 18 11:38:33 2020 +0900
+++ b/LEMC.agda	Sat Jul 18 12:29:38 2020 +0900
@@ -31,8 +31,6 @@
      is-in : X ∋ a-choice
 
 open HOD
-_=h=_ : (x y : HOD) → Set n
-x =h= y  = od x == od y
 
 open choiced
 
diff -r 67580311cc8e -r 7f919d6b045b OD.agda
--- a/OD.agda	Sat Jul 18 11:38:33 2020 +0900
+++ b/OD.agda	Sat Jul 18 12:29:38 2020 +0900
@@ -327,357 +327,353 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
+Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
+Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
+Replace : HOD  → (HOD  → HOD) → HOD 
+Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
+    ; odmax = rmax ; <odmax = rmax<} where 
+        rmax : Ordinal
+        rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
+        rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
+        rmax< lt = proj1 lt
+Union : HOD  → HOD   
+Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
+    ; odmax = osuc (od→ord U) ; <odmax = umax< } where
+        umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
+        umax< {y} not = lemma (FExists _ lemma1 not ) where
+            lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x
+            lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y))
+            lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U
+            lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U))
+            lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y)
+            lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
+            lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U)
+            lemma not with trio< y (od→ord U)
+            lemma not | tri< a ¬b ¬c = ordtrans a <-osuc
+            lemma not | tri≈ ¬a refl ¬c = <-osuc
+            lemma not | tri> ¬a ¬b c = ⊥-elim (not c)
+_∈_ : ( A B : HOD  ) → Set n
+A ∈ B = B ∋ A
+
+OPwr :  (A :  HOD ) → HOD 
+OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) )   
+
+Power : HOD  → HOD 
+Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
+-- ｛_｝ : ZFSet → ZFSet
+-- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
+
+data infinite-d  : ( x : Ordinal  ) → Set n where
+    iφ :  infinite-d o∅
+    isuc : {x : Ordinal  } →   infinite-d  x  →
+            infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
+
+-- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
+-- We simply assumes infinite-d y has a maximum.
+-- 
+-- This means that many of OD may not be HODs because of the od→ord mapping divergence.
+-- We should have some axioms to prevent this such as od→ord x o< next (odmax x).
+-- 
+postulate
+    ωmax : Ordinal
+    <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
+
+infinite : HOD 
+infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
+
+infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 
+infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
+    u : (y : Ordinal ) → HOD
+    u y = Union (ord→od y , (ord→od y , ord→od y))
+    --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+    lemma8 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
+    lemma8 = ho<
+    ---           (x,y) < next (omax x y) < next (osuc y) = next y 
+    lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
+    lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
+    lemma81 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
+    lemma81 {y} = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
+    lemma9 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
+    lemma9 = lemmaa (c<→o< (case1 refl))
+    lemma71 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
+    lemma71 = next< lemma81 lemma9
+    lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
+    lemma1 = ho<
+    --- main recursion
+    lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+    lemma {o∅} iφ = x<nx
+    lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
+
+ω<next-o∅ : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
+ω<next-o∅ ho< {y} lt = <odmax (infinite' ho<) lt
+
+nat→ω : Nat → HOD
+nat→ω Zero = od∅
+nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
+
+ω→nat : (n : HOD) → infinite ∋ n → Nat
+ω→nat n = lemma where
+    lemma : {y : Ordinal} → infinite-d y → Nat
+    lemma iφ = Zero
+    lemma (isuc lt) = Suc (lemma lt)
+
+ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
+ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ
+ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n}))
+
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
+infixr  200 _∈_
+-- infixr  230 _∩_ _∪_
+
+pair→ : ( x y t : HOD  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y ) 
+pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x ))
+pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y ))
+
+pair← : ( x y t : HOD  ) → ( t =h= x ) ∨ ( t =h= y ) →  (x , y)  ∋ t  
+pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x))
+pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y))
+
+empty : (x : HOD  ) → ¬  (od∅ ∋ x)
+empty x = ¬x<0 
+
+o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) 
+o<→c< lt = record { incl = λ z → ordtrans z lt }  
+
+⊆→o< :  {x y : Ordinal } → (Ord x) ⊆ (Ord y) →  x o< osuc y
+⊆→o< {x} {y}  lt with trio< x y 
+⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
+⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
+⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym diso) refl )
+... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
+
+union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
+    ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
+union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+union← X z UX∋z =  FExists _ lemma UX∋z where
+    lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
+    lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 
+
+ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
+ψiso {ψ} t refl = t
+selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+selection {ψ} {X} {y} = record {
+    proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
+  ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
+  }
+sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
+sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
+replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
+replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; proj2 = lemma } where 
+    lemma : def (in-codomain X ψ) (od→ord (ψ x))
+    lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
+replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
+replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
+    lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
+            → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)))
+    lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
+        lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) =h= ψ (ord→od y))  
+        lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
+    lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) )
+    lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso  ( proj2 not2 ))
+
+---
+--- Power Set
+---
+---    First consider ordinals in HOD
+---
+--- A ∩ x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
+--
+--
+∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
+∩-≡ {a} {b} inc = record {
+   eq→ = λ {x} x<a → record { proj2 = x<a ;
+        proj1 = odef-subst  {_} {_} {b} {x} (inc (odef-subst  {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
+   eq← = λ {x} x<a∩b → proj2 x<a∩b }
+-- 
+-- Transitive Set case
+-- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
+-- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
+-- OPwr  A = Ord ( sup-o ( λ x → od→ord ( A ∩ (ord→od x )) ) )   
+-- 
+ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
+ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {od→ord t}
+        lemma refl (lemma1 lemma-eq )where
+    lemma-eq :  ((Ord a) ∩ t) =h= t
+    eq→ lemma-eq {z} w = proj2 w 
+    eq← lemma-eq {z} w = record { proj2 = w  ;
+        proj1 = odef-subst  {_} {_} {(Ord a)} {z}
+        ( t→A (odef-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
+    lemma1 :  {a : Ordinal } { t : HOD }
+        → (eq : ((Ord a) ∩ t) =h= t)  → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t
+    lemma1  {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
+    lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
+    lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) 
+    lemma :  od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x)))
+    lemma = sup-o< _ lemma2
+
+-- 
+-- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
+-- then replace of all elements of the Power set by A ∩ y
+-- 
+-- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y )
+
+-- we have oly double negation form because of the replacement axiom
+--
+power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
+power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
+    a = od→ord A
+    lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
+    lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t
+    lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
+    lemma3 y eq not = not (proj1 (eq→ eq t∋x))
+    lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y)))
+    lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 ))
+    lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) →  ¬ ¬  (odef A (od→ord x))
+    lemma5 {y} eq not = (lemma3 (ord→od y) eq) not
+
+power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 
+    a = od→ord A
+    lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
+    lemma0 {x} t∋x = c<→o< (t→A t∋x)
+    lemma3 : OPwr (Ord a) ∋ t
+    lemma3 = ord-power← a t lemma0
+    lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
+    lemma4 = let open ≡-Reasoning in begin
+        A ∩ ord→od (od→ord t)
+        ≡⟨ cong (λ k → A ∩ k) oiso ⟩
+        A ∩ t
+        ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩
+        t
+        ∎
+    sup1 : Ordinal
+    sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x)))
+    lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
+    lemma9 = <-osuc 
+    lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
+    lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 
+    lemmad : Ord (osuc (od→ord A)) ∋ t
+    lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) 
+    lemmac : ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A)
+    lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
+        lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
+        lemmaf {x} lt = proj1 lt
+        lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x
+        lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } 
+    lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
+    lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
+    lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
+    lemma7 with osuc-≡< lemmad
+    lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
+    lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where
+        lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x
+        lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t))
+            diso
+            (c<→o< (subst₂ (λ j k → def (od j)  k) oiso (sym diso) lt )))
+    lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where 
+        lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t
+        lemmai = let open ≡-Reasoning in begin
+                od→ord (Ord (od→ord A)) 
+            ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩
+                od→ord (Ord (od→ord t)) 
+            ≡⟨ sym diso ⟩
+                od→ord (ord→od (od→ord (Ord (od→ord t))))
+            ≡⟨ sym eq1 ⟩
+                od→ord (ord→od (od→ord t))
+            ≡⟨ diso ⟩
+                od→ord t 
+            ∎
+    lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where
+        lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A))
+        lemmak = let open ≡-Reasoning in begin
+                od→ord (ord→od (od→ord (Ord (od→ord t))))
+            ≡⟨ diso ⟩
+                od→ord (Ord (od→ord t))
+            ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩
+                od→ord (Ord (od→ord A))
+            ∎
+        lemmaj : od→ord t o< od→ord (Ord (od→ord A))
+        lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt 
+    lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
+    lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
+        lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
+    lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
+    lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
+        lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
+        lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A  )))
+
+
+ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 
+ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
+    lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
+    lemma lt y<x with osuc-≡< lt
+    lemma lt y<x | case1 refl = c<→o< y<x
+    lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
+
+continuum-hyphotheis : (a : Ordinal) → Set (suc n)
+continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)
+
+extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B
+eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
+eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+
+extensionality : {A B w : HOD  } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
+proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
+proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
+
+infinity∅ : infinite  ∋ od∅ 
+infinity∅ = odef-subst  {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
+    lemma : o∅ ≡ od→ord od∅
+    lemma =  let open ≡-Reasoning in begin
+        o∅
+        ≡⟨ sym diso ⟩
+        od→ord ( ord→od o∅ )
+        ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
+        od→ord od∅
+        ∎
+infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
+infinity x lt = odef-subst  {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
+    lemma :  od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
+        ≡ od→ord (Union (x , (x , x)))
+    lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 
+
+isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
+isZF = record {
+        isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
+    ;   pair→  = pair→
+    ;   pair←  = pair←
+    ;   union→ = union→
+    ;   union← = union←
+    ;   empty = empty
+    ;   power→ = power→  
+    ;   power← = power← 
+    ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 
+    ;   ε-induction = ε-induction 
+    ;   infinity∅ = infinity∅
+    ;   infinity = infinity
+    ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
+    ;   replacement← = replacement←
+    ;   replacement→ = λ {ψ} → replacement→ {ψ}
+    -- ;   choice-func = choice-func
+    -- ;   choice = choice
+    } 
+
 HOD→ZF : ZF  
 HOD→ZF   = record { 
     ZFSet = HOD 
     ; _∋_ = _∋_ 
-    ; _≈_ = hod→zf._=h=_ 
+    ; _≈_ = _=h=_ 
     ; ∅  = od∅
     ; _,_ = _,_
-    ; Union = hod→zf.Union
-    ; Power = hod→zf.Power
-    ; Select = hod→zf.Select
-    ; Replace = hod→zf.Replace
-    ; infinite = hod→zf.infinite
-    ; isZF = hod→zf.isZF 
- } where
-  module hod→zf where
-    ZFSet = HOD             -- is less than Ords because of maxod
-    Select : (X : HOD  ) → ((x : HOD  ) → Set n ) → HOD 
-    Select X ψ = record { od = record { def = λ x →  ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
-    Replace : HOD  → (HOD  → HOD) → HOD 
-    Replace X ψ = record { od = record { def = λ x → (x o< sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))) ∧ def (in-codomain X ψ) x }
-       ; odmax = rmax ; <odmax = rmax<} where 
-          rmax : Ordinal
-          rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
-          rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
-          rmax< lt = proj1 lt
-    Union : HOD  → HOD   
-    Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
-       ; odmax = osuc (od→ord U) ; <odmax = umax< } where
-           umax< :  {y : Ordinal} → ¬ ((u : Ordinal) → ¬ def (od U) u ∧ def (od (ord→od u)) y) → y o< osuc (od→ord U)
-           umax< {y} not = lemma (FExists _ lemma1 not ) where
-               lemma0 : {x : Ordinal} → def (od (ord→od x)) y → y o< x
-               lemma0 {x} x<y = subst₂ (λ j k → j o< k ) diso  diso (c<→o< (subst (λ k → def (od (ord→od x)) k) (sym diso) x<y))
-               lemma2 : {x : Ordinal} → def (od U) x → x o< od→ord U
-               lemma2 {x} x<U = subst (λ k → k o< od→ord U ) diso (c<→o< (subst (λ k → def (od U) k) (sym diso) x<U))
-               lemma1 : {x : Ordinal} → def (od U) x ∧ def (od (ord→od x)) y → ¬ (od→ord U o< y)
-               lemma1 {x} lt u<y = o<> u<y (ordtrans (lemma0 (proj2 lt)) (lemma2 (proj1 lt)) )
-               lemma : ¬ ((od→ord U) o< y ) → y o< osuc (od→ord U)
-               lemma not with trio< y (od→ord U)
-               lemma not | tri< a ¬b ¬c = ordtrans a <-osuc
-               lemma not | tri≈ ¬a refl ¬c = <-osuc
-               lemma not | tri> ¬a ¬b c = ⊥-elim (not c)
-    _∈_ : ( A B : ZFSet  ) → Set n
-    A ∈ B = B ∋ A
-
-    OPwr :  (A :  HOD ) → HOD 
-    OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) )   
-
-    Power : HOD  → HOD 
-    Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
-    -- ｛_｝ : ZFSet → ZFSet
-    -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
-
-    data infinite-d  : ( x : Ordinal  ) → Set n where
-        iφ :  infinite-d o∅
-        isuc : {x : Ordinal  } →   infinite-d  x  →
-                infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
-
-    -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
-    -- We simply assumes infinite-d y has a maximum.
-    -- 
-    -- This means that many of OD may not be HODs because of the od→ord mapping divergence.
-    -- We should have some axioms to prevent this such as od→ord x o< next (odmax x).
-    -- 
-    postulate
-        ωmax : Ordinal
-        <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
-
-    infinite : HOD 
-    infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax } 
-
-    infinite' : ({x : HOD} → od→ord x o< next (odmax x)) → HOD 
-    infinite' ho< = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
-        u : (y : Ordinal ) → HOD
-        u y = Union (ord→od y , (ord→od y , ord→od y))
-        --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-        lemma8 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (odmax (ord→od y , ord→od y))
-        lemma8 = ho<
-        ---           (x,y) < next (omax x y) < next (osuc y) = next y 
-        lemmaa : {x y : HOD} → od→ord x o< od→ord y → od→ord (x , y) o< next (od→ord y)
-        lemmaa {x} {y} x<y = subst (λ k → od→ord (x , y) o< k ) (sym nexto≡) (subst (λ k → od→ord (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
-        lemma81 : {y : Ordinal} → od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
-        lemma81 {y} = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-        lemma9 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y , ord→od y))
-        lemma9 = lemmaa (c<→o< (case1 refl))
-        lemma71 : {y : Ordinal} → od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
-        lemma71 = next< lemma81 lemma9
-        lemma1 : {y : Ordinal} → od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
-        lemma1 = ho<
-        --- main recursion
-        lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-        lemma {o∅} iφ = x<nx
-        lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
-
-    nat→ω : Nat → HOD
-    nat→ω Zero = od∅
-    nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
-
-    ω→nat : (n : HOD) → infinite ∋ n → Nat
-    ω→nat n = lemma where
-        lemma : {y : Ordinal} → infinite-d y → Nat
-        lemma iφ = Zero
-        lemma (isuc lt) = Suc (lemma lt)
-
-    ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
-    ω∋nat→ω {Zero} = subst (λ k → def (od infinite) k) {!!} iφ
-    ω∋nat→ω {Suc n} = subst (λ k → def (od infinite) k) {!!} (isuc ( ω∋nat→ω {n}))
-
-    _=h=_ : (x y : HOD) → Set n
-    x =h= y  = od x == od y
-
-    infixr  200 _∈_
-    -- infixr  230 _∩_ _∪_
-    isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
-    isZF = record {
-           isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
-       ;   pair→  = pair→
-       ;   pair←  = pair←
-       ;   union→ = union→
-       ;   union← = union←
-       ;   empty = empty
-       ;   power→ = power→  
-       ;   power← = power← 
-       ;   extensionality = λ {A} {B} {w} → extensionality {A} {B} {w} 
-       ;   ε-induction = ε-induction 
-       ;   infinity∅ = infinity∅
-       ;   infinity = infinity
-       ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
-       ;   replacement← = replacement←
-       ;   replacement→ = λ {ψ} → replacement→ {ψ}
-       -- ;   choice-func = choice-func
-       -- ;   choice = choice
-     } where
-
-         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t =h= x ) ∨ ( t =h= y ) 
-         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡x ))
-         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j =h= k ) oiso oiso (o≡→== t≡y ))
-
-         pair← : ( x y t : ZFSet  ) → ( t =h= x ) ∨ ( t =h= y ) →  (x , y)  ∋ t  
-         pair← x y t (case1 t=h=x) = case1 (cong (λ k → od→ord k ) (==→o≡ t=h=x))
-         pair← x y t (case2 t=h=y) = case2 (cong (λ k → od→ord k ) (==→o≡ t=h=y))
-
-         empty : (x : HOD  ) → ¬  (od∅ ∋ x)
-         empty x = ¬x<0 
-
-         o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) 
-         o<→c< lt = record { incl = λ z → ordtrans z lt }  
-         
-         ⊆→o< :  {x y : Ordinal } → (Ord x) ⊆ (Ord y) →  x o< osuc y
-         ⊆→o< {x} {y}  lt with trio< x y 
-         ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
-         ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
-         ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with (incl lt)  (o<-subst c (sym diso) refl )
-         ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
-
-         union→ :  (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
-         union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
-              ; proj2 = subst ( λ k → odef k (od→ord z)) (sym oiso) (proj2 xx) } ))
-         union← :  (X z : HOD) (X∋z : Union X ∋ z) →  ¬  ( (u : HOD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
-         union← X z UX∋z =  FExists _ lemma UX∋z where
-              lemma : {y : Ordinal} → odef X y ∧ odef (ord→od y) (od→ord z) → ¬ ((u : HOD) → ¬ (X ∋ u) ∧ (u ∋ z))
-              lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → odef X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 
+    ; Union = Union
+    ; Power = Power
+    ; Select = Select
+    ; Replace = Replace
+    ; infinite = infinite
+    ; isZF = isZF 
+ } 
+  
 
-         ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
-         ψiso {ψ} t refl = t
-         selection : {ψ : HOD → Set n} {X y : HOD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
-         selection {ψ} {X} {y} = record {
-              proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso)  }
-            ; proj2 = λ select → record { proj1 = proj1 select  ; proj2 =  ψiso {ψ} (proj2 select) oiso  }
-           }
-         sup-c< :  (ψ : HOD → HOD) → {X x : HOD} → X ∋ x  → od→ord (ψ x) o< (sup-o X (λ y X∋y → od→ord (ψ (ord→od y))))
-         sup-c< ψ {X} {x} lt = subst (λ k → od→ord (ψ k) o< _ ) oiso (sup-o< X lt )
-         replacement← : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {X} {x} lt ; proj2 = lemma } where 
-             lemma : def (in-codomain X ψ) (od→ord (ψ x))
-             lemma not = ⊥-elim ( not ( od→ord x ) (record { proj1 = lt ; proj2 = cong (λ k → od→ord (ψ k)) (sym oiso)} ))
-         replacement→ : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
-         replacement→ {ψ} X x lt = contra-position lemma (lemma2 (proj2 lt)) where
-            lemma2 :  ¬ ((y : Ordinal) → ¬ odef X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
-                    → ¬ ((y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)))
-            lemma2 not not2  = not ( λ y d →  not2 y (record { proj1 = proj1 d ; proj2 = lemma3 (proj2 d)})) where
-                lemma3 : {y : Ordinal } → (od→ord x ≡ od→ord (ψ (ord→od  y))) → (ord→od (od→ord x) =h= ψ (ord→od y))  
-                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) =h= k ) oiso (o≡→== eq )
-            lemma :  ( (y : HOD) → ¬ (x =h= ψ y)) → ( (y : Ordinal) → ¬ odef X y ∧ (ord→od (od→ord x) =h= ψ (ord→od y)) )
-            lemma not y not2 = not (ord→od y) (subst (λ k → k =h= ψ (ord→od y)) oiso  ( proj2 not2 ))
-
-         ---
-         --- Power Set
-         ---
-         ---    First consider ordinals in HOD
-         ---
-         --- A ∩ x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
-         --
-         --
-         ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
-         ∩-≡ {a} {b} inc = record {
-            eq→ = λ {x} x<a → record { proj2 = x<a ;
-                 proj1 = odef-subst  {_} {_} {b} {x} (inc (odef-subst  {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
-            eq← = λ {x} x<a∩b → proj2 x<a∩b }
-         -- 
-         -- Transitive Set case
-         -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
-         -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
-         -- OPwr  A = Ord ( sup-o ( λ x → od→ord ( A ∩ (ord→od x )) ) )   
-         -- 
-         ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
-         ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {od→ord t}
-                 lemma refl (lemma1 lemma-eq )where
-              lemma-eq :  ((Ord a) ∩ t) =h= t
-              eq→ lemma-eq {z} w = proj2 w 
-              eq← lemma-eq {z} w = record { proj2 = w  ;
-                 proj1 = odef-subst  {_} {_} {(Ord a)} {z}
-                    ( t→A (odef-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
-              lemma1 :  {a : Ordinal } { t : HOD }
-                 → (eq : ((Ord a) ∩ t) =h= t)  → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t
-              lemma1  {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-              lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
-              lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) 
-              lemma :  od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x)))
-              lemma = sup-o< _ lemma2
-
-         -- 
-         -- Every set in HOD is a subset of Ordinals, so make OPwr (Ord (od→ord A)) first
-         -- then replace of all elements of the Power set by A ∩ y
-         -- 
-         -- Power A = Replace (OPwr (Ord (od→ord A))) ( λ y → A ∩ y )
-
-         -- we have oly double negation form because of the replacement axiom
-         --
-         power→ :  ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → ¬ ¬ (A ∋ x)
-         power→ A t P∋t {x} t∋x = FExists _ lemma5 lemma4 where
-              a = od→ord A
-              lemma2 : ¬ ( (y : HOD) → ¬ (t =h=  (A ∩ y)))
-              lemma2 = replacement→ {λ x → A ∩ x} (OPwr (Ord (od→ord A))) t P∋t
-              lemma3 : (y : HOD) → t =h= ( A ∩ y ) → ¬ ¬ (A ∋ x)
-              lemma3 y eq not = not (proj1 (eq→ eq t∋x))
-              lemma4 : ¬ ((y : Ordinal) → ¬ (t =h= (A ∩ ord→od y)))
-              lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t =h= ( A ∩ k )) (sym oiso) not1 ))
-              lemma5 : {y : Ordinal} → t =h= (A ∩ ord→od y) →  ¬ ¬  (odef A (od→ord x))
-              lemma5 {y} eq not = (lemma3 (ord→od y) eq) not
-
-         power← :  (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
-         power← A t t→A = record { proj1 = lemma1 ; proj2 = lemma2 } where 
-              a = od→ord A
-              lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
-              lemma0 {x} t∋x = c<→o< (t→A t∋x)
-              lemma3 : OPwr (Ord a) ∋ t
-              lemma3 = ord-power← a t lemma0
-              lemma4 :  (A ∩ ord→od (od→ord t)) ≡ t
-              lemma4 = let open ≡-Reasoning in begin
-                    A ∩ ord→od (od→ord t)
-                 ≡⟨ cong (λ k → A ∩ k) oiso ⟩
-                    A ∩ t
-                 ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩
-                    t
-                 ∎
-              sup1 : Ordinal
-              sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x)))
-              lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
-              lemma9 = <-osuc 
-              lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
-              lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 
-              lemmad : Ord (osuc (od→ord A)) ∋ t
-              lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) 
-              lemmac : ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A)
-              lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
-                 lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
-                 lemmaf {x} lt = proj1 lt
-                 lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x
-                 lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } 
-              lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
-              lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
-              lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
-              lemma7 with osuc-≡< lemmad
-              lemma7 | case2 lt = ordtrans (c<→o< lt) (subst (λ k → k o< sup1) lemmae lemmab )
-              lemma7 | case1 eq with osuc-≡< (⊆→o≤ {ord→od (od→ord t)} {ord→od (od→ord (Ord (od→ord t)))} (λ {x} lt → lemmah lt )) where
-                  lemmah : {x : Ordinal } → def (od (ord→od (od→ord t))) x → def (od (ord→od (od→ord (Ord (od→ord t))))) x
-                  lemmah {x} lt = subst (λ k → def (od k) x ) (sym oiso) (subst (λ k → k o< (od→ord t))
-                      diso
-                      (c<→o< (subst₂ (λ j k → def (od j)  k) oiso (sym diso) lt )))
-              lemma7 | case1 eq | case1 eq1 = subst (λ k → k o< sup1) (trans lemmae lemmai) lemmab where 
-                  lemmai : od→ord (Ord (od→ord A)) ≡ od→ord t
-                  lemmai = let open ≡-Reasoning in begin
-                           od→ord (Ord (od→ord A)) 
-                        ≡⟨ sym (cong (λ k → od→ord (Ord k)) eq) ⟩
-                           od→ord (Ord (od→ord t)) 
-                        ≡⟨ sym diso ⟩
-                           od→ord (ord→od (od→ord (Ord (od→ord t))))
-                        ≡⟨ sym eq1 ⟩
-                           od→ord (ord→od (od→ord t))
-                        ≡⟨ diso ⟩
-                           od→ord t 
-                        ∎
-              lemma7 | case1 eq | case2 lt = ordtrans lemmaj (subst (λ k → k o< sup1) lemmae lemmab ) where
-                  lemmak : od→ord (ord→od (od→ord (Ord (od→ord t)))) ≡ od→ord (Ord (od→ord A))
-                  lemmak = let open ≡-Reasoning in begin
-                           od→ord (ord→od (od→ord (Ord (od→ord t))))
-                        ≡⟨ diso ⟩
-                           od→ord (Ord (od→ord t))
-                        ≡⟨ cong (λ k → od→ord (Ord k)) eq ⟩
-                           od→ord (Ord (od→ord A))
-                        ∎
-                  lemmaj : od→ord t o< od→ord (Ord (od→ord A))
-                  lemmaj = subst₂ (λ j k → j o< k ) diso lemmak lt 
-              lemma1 : od→ord t o< sup-o (OPwr (Ord (od→ord A))) (λ x lt → od→ord (A ∩ (ord→od x)))
-              lemma1 = subst (λ k → od→ord k o< sup-o (OPwr (Ord (od→ord A)))  (λ x lt → od→ord (A ∩ (ord→od x))))
-                  lemma4 (sup-o< (OPwr (Ord (od→ord A))) lemma7 )
-              lemma2 :  def (in-codomain (OPwr (Ord (od→ord A))) (_∩_ A)) (od→ord t)
-              lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
-                  lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
-                  lemma6 = cong ( λ k → od→ord k ) (==→o≡ (subst (λ k → t =h= (A ∩ k)) (sym oiso) ( ∩-≡ {t} {A} t→A  )))
-
-
-         ord⊆power : (a : Ordinal) → (Ord (osuc a)) ⊆ (Power (Ord a)) 
-         ord⊆power a = record { incl = λ {x} lt →  power← (Ord a) x (lemma lt) } where
-                lemma : {x y : HOD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
-                lemma lt y<x with osuc-≡< lt
-                lemma lt y<x | case1 refl = c<→o< y<x
-                lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
-
-         continuum-hyphotheis : (a : Ordinal) → Set (suc n)
-         continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)
-
-         extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A =h= B
-         eq→ (extensionality0 {A} {B} eq ) {x} d = odef-iso  {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
-         eq← (extensionality0 {A} {B} eq ) {x} d = odef-iso  {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
-
-         extensionality : {A B w : HOD  } → ((z : HOD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
-         proj1 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) ( ==→o≡ (extensionality0 {A} {B} eq) ) d
-         proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
-
-         infinity∅ : infinite  ∋ od∅ 
-         infinity∅ = odef-subst  {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
-              lemma : o∅ ≡ od→ord od∅
-              lemma =  let open ≡-Reasoning in begin
-                    o∅
-                 ≡⟨ sym diso ⟩
-                    od→ord ( ord→od o∅ )
-                 ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
-                    od→ord od∅
-                 ∎
-         infinity : (x : HOD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x lt = odef-subst  {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
-               lemma :  od→ord (Union (ord→od (od→ord x) , (ord→od (od→ord x) , ord→od (od→ord x))))
-                    ≡ od→ord (Union (x , (x , x)))
-               lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 
-
-
-Union = ZF.Union HOD→ZF
-Power = ZF.Power HOD→ZF
-Select = ZF.Select HOD→ZF
-Replace = ZF.Replace HOD→ZF
-infinite = ZF.infinite HOD→ZF
-isZF = ZF.isZF  HOD→ZF
-
diff -r 67580311cc8e -r 7f919d6b045b ODC.agda
--- a/ODC.agda	Sat Jul 18 11:38:33 2020 +0900
+++ b/ODC.agda	Sat Jul 18 12:29:38 2020 +0900
@@ -25,9 +25,6 @@
 
 open _∧_
 
-_=h=_ : (x y : HOD) → Set n
-x =h= y  = od x == od y
-
 postulate      
   -- mimimul and x∋minimal is an Axiom of choice
   minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
diff -r 67580311cc8e -r 7f919d6b045b OPair.agda
--- a/OPair.agda	Sat Jul 18 11:38:33 2020 +0900
+++ b/OPair.agda	Sat Jul 18 12:29:38 2020 +0900
@@ -28,9 +28,6 @@
 
 open _==_
 
-_=h=_ : (x y : HOD) → Set n
-x =h= y  = od x == od y
-
 <_,_> : (x y : HOD) → HOD
 < x , y > = (x , x ) , (x , y )
 
diff -r 67580311cc8e -r 7f919d6b045b filter.agda
--- a/filter.agda	Sat Jul 18 11:38:33 2020 +0900
+++ b/filter.agda	Sat Jul 18 12:29:38 2020 +0900
@@ -71,8 +71,6 @@
 q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
 open HOD
-_=h=_ : (x y : HOD) → Set n
-x =h= y  = od x == od y
 
 -----
 --
@@ -157,16 +155,9 @@
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
 
-nat→ω : Nat → HOD
-nat→ω Zero = od∅
-nat→ω (Suc y) = Union (nat→ω y , (nat→ω y , nat→ω y)) 
+postulate  
+   ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 
 
-postulate  -- we have proved in other module
-   ω∋nat→ω : {n : Nat} → def (od infinite) (od→ord (nat→ω n))
-   ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
-
-postulate
-   ho< : {x : HOD} → hod-ord< {x} -- : ({x : HOD} → od→ord x o< next (odmax x)) 
 
 data Hω2 : ( x : Ordinal  ) → Set n where
   hφ :  Hω2 o∅
@@ -179,6 +170,8 @@
 
 HODω2 :  HOD
 HODω2 = record { od = record { def = λ x → Hω2 x } ; odmax = next o∅ ; <odmax = odmax0 } where
+    ω<next : {y : Ordinal} → infinite-d y → y o< next o∅
+    ω<next = ω<next-o∅ ho<
     lemma0 : {n y : Ordinal} → Hω2 y → odef infinite n  → od→ord < ord→od n , ord→od y > o< next y
     lemma0 {n} {y} hw2 inf = nexto=n {!!} 
     odmax0 : {y : Ordinal} → Hω2 y → y o< next o∅
@@ -187,6 +180,22 @@
     odmax0 (h1 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {1} )))
     odmax0 (h2 {y} lt) = next< (odmax0 lt) (subst (λ k → k o< next y ) (cong (λ k →  od→ord < k , ord→od y >) oiso )  (lemma0 lt (ω∋nat→ω {2} )))
 
+HODω2-Filter : Filter HODω2
+HODω2-Filter = record {
+       filter = {!!}
+     ; f⊆PL = {!!}
+     ; filter1 = {!!}
+     ; filter2 = {!!}
+   } where
+       filter0 : HOD   
+       filter0 = {!!}
+       f⊆PL1 :  filter0 ⊆ Power HODω2 
+       f⊆PL1 = {!!}
+       filter11 : { p q : HOD } →  q ⊆ HODω2  → filter0 ∋ p →  p ⊆ q  → filter0 ∋ q
+       filter11 = {!!}
+       filter12 : { p q : HOD } → filter0 ∋ p →  filter0 ∋ q  → filter0 ∋ (p ∩ q)
+       filter12 = {!!}
+
 -- the set of finite partial functions from ω to 2
 
 data Two : Set n where