# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593935953 -32400
# Node ID ba3ebb9a16c68a42615322daab3b1563bd9bcfe2
# Parent  9f926b2210bc8d1869b5abd4df07c1c12faa3bcf# Parent  214a087c78a5bdb15fddc4db038bd9c179750344
HOD

diff -r 9f926b2210bc -r ba3ebb9a16c6 .hgtags
diff -r 9f926b2210bc -r ba3ebb9a16c6 BAlgbra.agda
--- a/BAlgbra.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/BAlgbra.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -19,60 +19,66 @@
 open OD O
 open OD.OD
 open ODAxiom odAxiom
+open HOD
 
 open _∧_
 open _∨_
 open Bool
 
-_∩_ : ( A B : OD  ) → OD
-A ∩ B = record { def = λ x → def A x ∧ def B x } 
-
-_∪_ : ( A B : OD  ) → OD
-A ∪ B = record { def = λ x → def A x ∨ def B x } 
+_∩_ : ( A B : HOD  ) → HOD
+A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
+    odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
 
-_＼_ : ( A B : OD  ) → OD
-A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
+_∪_ : ( A B : HOD  ) → HOD
+A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
+    odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
+      lemma :  {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
+      lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
+      lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
 
-∪-Union : { A B : OD } → Union (A , B) ≡ ( A ∪ B )
+_＼_ : ( A B : HOD  ) → HOD
+A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
+
+∪-Union : { A B : HOD } → Union (A , B) ≡ ( A ∪ B )
 ∪-Union {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } )  where
-    lemma1 :  {x : Ordinal} → def (Union (A , B)) x → def (A ∪ B) x
+    lemma1 :  {x : Ordinal} → odef (Union (A , B)) x → odef (A ∪ B) x
     lemma1 {x} lt = lemma3 lt where
-        lemma4 : {y : Ordinal} → def (A , B) y ∧ def (ord→od y) x → ¬ (¬ ( def A x ∨ def B x) )
+        lemma4 : {y : Ordinal} → odef (A , B) y ∧ odef (ord→od y) x → ¬ (¬ ( odef A x ∨ odef B x) )
         lemma4 {y} z with proj1 z
-        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
-        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
-        lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
+        lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → odef k x ) oiso (proj2 z)) )
+        lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → odef k x ) oiso (proj2 z)) )
+        lemma3 : (((u : Ordinals.ord O) → ¬ odef (A , B) u ∧ odef (ord→od u) x) → ⊥) → odef (A ∪ B) x
         lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
-    lemma2 :  {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
-    lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
-       (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
-    lemma2 {x} (case2 B∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
-       (record { proj1 = case2 refl ; proj2 = subst (λ k → def B k) (sym diso) B∋x}))
+    lemma2 :  {x : Ordinal} → odef (A ∪ B) x → odef (Union (A , B)) x
+    lemma2 {x} (case1 A∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
+       (record { proj1 = case1 refl ; proj2 = subst (λ k → odef A k) (sym diso) A∋x}))
+    lemma2 {x} (case2 B∋x) = subst (λ k → odef (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) B
+       (record { proj1 = case2 refl ; proj2 = subst (λ k → odef B k) (sym diso) B∋x}))
 
-∩-Select : { A B : OD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
+∩-Select : { A B : HOD } →  Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  ) ≡ ( A ∩ B )
 ∩-Select {A} {B} = ==→o≡ ( record { eq→ =  lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → def (A ∩ B) x
-    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → def B k ) diso (proj2 (proj2 lt)) }
-    lemma2 : {x : Ordinal} → def (A ∩ B) x → def (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
+    lemma1 : {x : Ordinal} → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x → odef (A ∩ B) x
+    lemma1 {x} lt = record { proj1 = proj1 lt ; proj2 = subst (λ k → odef B k ) diso (proj2 (proj2 lt)) }
+    lemma2 : {x : Ordinal} → odef (A ∩ B) x → odef (Select A (λ x₁ → (A ∋ x₁) ∧ (B ∋ x₁))) x
     lemma2 {x} lt = record { proj1 = proj1 lt ; proj2 =
-        record { proj1 = subst (λ k → def A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → def B k ) (sym diso) (proj2 lt) } }
+        record { proj1 = subst (λ k → odef A k) (sym diso) (proj1 lt) ; proj2 = subst (λ k → odef B k ) (sym diso) (proj2 lt) } }
 
-dist-ord : {p q r : OD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
+dist-ord : {p q r : HOD } → p ∩ ( q ∪ r ) ≡   ( p ∩ q ) ∪ ( p ∩ r )
 dist-ord {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-    lemma1 :  {x : Ordinal} → def (p ∩ (q ∪ r)) x → def ((p ∩ q) ∪ (p ∩ r)) x
+    lemma1 :  {x : Ordinal} → odef (p ∩ (q ∪ r)) x → odef ((p ∩ q) ∪ (p ∩ r)) x
     lemma1 {x} lt with proj2 lt
     lemma1 {x} lt | case1 q∋x = case1 ( record { proj1 = proj1 lt ; proj2 = q∋x } )
     lemma1 {x} lt | case2 r∋x = case2 ( record { proj1 = proj1 lt ; proj2 = r∋x } )
-    lemma2  : {x : Ordinal} → def ((p ∩ q) ∪ (p ∩ r)) x → def (p ∩ (q ∪ r)) x
+    lemma2  : {x : Ordinal} → odef ((p ∩ q) ∪ (p ∩ r)) x → odef (p ∩ (q ∪ r)) x
     lemma2 {x} (case1 p∩q) = record { proj1 = proj1 p∩q ; proj2 = case1 (proj2 p∩q ) } 
     lemma2 {x} (case2 p∩r) = record { proj1 = proj1 p∩r ; proj2 = case2 (proj2 p∩r ) } 
 
-dist-ord2 : {p q r : OD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
+dist-ord2 : {p q r : HOD } → p ∪ ( q ∩ r ) ≡   ( p ∪ q ) ∩ ( p ∪ r )
 dist-ord2 {p} {q} {r} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-    lemma1 : {x : Ordinal} → def (p ∪ (q ∩ r)) x → def ((p ∪ q) ∩ (p ∪ r)) x
+    lemma1 : {x : Ordinal} → odef (p ∪ (q ∩ r)) x → odef ((p ∪ q) ∩ (p ∪ r)) x
     lemma1 {x} (case1 cp) = record { proj1 = case1 cp ; proj2 = case1 cp }
     lemma1 {x} (case2 cqr) = record { proj1 = case2 (proj1 cqr) ; proj2 = case2 (proj2 cqr) }
-    lemma2 : {x : Ordinal} → def ((p ∪ q) ∩ (p ∪ r)) x → def (p ∪ (q ∩ r)) x
+    lemma2 : {x : Ordinal} → odef ((p ∪ q) ∩ (p ∪ r)) x → odef (p ∪ (q ∩ r)) x
     lemma2 {x} lt with proj1 lt | proj2 lt
     lemma2 {x} lt | case1 cp | _ = case1 cp
     lemma2 {x} lt | _ | case1 cp = case1 cp 
diff -r 9f926b2210bc -r ba3ebb9a16c6 LEMC.agda
--- a/LEMC.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/LEMC.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -23,38 +23,42 @@
 
 open import zfc
 
---- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+--- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
 ---
-record choiced  ( X : OD) : Set (suc n) where
+record choiced  ( X : HOD) : Set (suc n) where
   field
-     a-choice : OD
+     a-choice : HOD
      is-in : X ∋ a-choice
 
+open HOD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
 open choiced
 
 OD→ZFC : ZFC
 OD→ZFC   = record { 
-    ZFSet = OD 
+    ZFSet = HOD 
     ; _∋_ = _∋_ 
-    ; _≈_ = _==_ 
+    ; _≈_ = _=h=_ 
     ; ∅  = od∅
     ; Select = Select
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select 
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select 
     isZFC = record {
        choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
        choice = λ A {X} A∋X not → is-in (choice-func X not)
      } where
-         choice-func :  (X : OD ) → ¬ ( X == od∅ ) → choiced X
+         choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X
          choice-func  X not = have_to_find where
                  ψ : ( ox : Ordinal ) → Set (suc n)
-                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced X
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite {ψ} induction ox where
-                    ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
+                 lemma-ord  ox = TransFinite1 {ψ} induction ox where
+                    ∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
                     ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
                     ∋-p A x | case1 (lift t)  = yes t
                     ∋-p A x | case2 t  = no (λ x → t (lift x ))
@@ -71,59 +75,61 @@
                     induction x prev with ∋-p X ( ord→od x) 
                     ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
                     ... | no ¬p = lemma where
-                         lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
+                         lemma1 : (y : Ordinal) → (y o< x → odef X y → ⊥) ∨ choiced X
                          lemma1 y with ∋-p X (ord→od y)
                          lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
-                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
-                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef X y → ⊥) ∨ choiced X
                          lemma = ∀-imply-or lemma1
                  have_to_find : choiced X
                  have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
-                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
+                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
                      ¬¬X∋x nn = not record {
-                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                         }
-         record Minimal (x : OD)  : Set (suc n) where
+         record Minimal (x : HOD)  : Set (suc n) where
            field
-               min : OD
+               min : HOD
                x∋min :   x ∋ min 
-               min-empty :  (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
+               min-empty :  (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
          open Minimal
          open _∧_
          --
          --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
          --
-         induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u )
-              →  (u : OD ) → (u∋x : u ∋ x) → Minimal u 
-         induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y))
+         induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
+              →  (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
+         induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
          ... | case1 P =
               record { min = x
                 ;     x∋min = u∋x
                 ;     min-empty = P
               } 
          ... | case2 NP =  min2 where
-              p : OD
-              p  = record { def = λ y1 → def x  y1 ∧ def u y1 }
-              np : ¬ (p == od∅)
-              np p∅ =  NP (λ y p∋y → ∅< p∋y p∅ ) 
+              p : HOD
+              p  = record { od = record { def = λ y1 → odef x  y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
+                 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
+                 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
+              np : ¬ (p =h= od∅)
+              np p∅ =  NP (λ y p∋y → ∅< {p} {_} p∋y p∅ ) 
               y1choice : choiced p
               y1choice = choice-func p np
-              y1 : OD
+              y1 : HOD
               y1 = a-choice y1choice
               y1prop : (x ∋ y1) ∧ (u ∋ y1)
               y1prop = is-in y1choice
               min2 : Minimal u
               min2 = prev (proj1 y1prop) u (proj2 y1prop)
-         Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u 
-         Min2 x u u∋x = (ε-induction {λ y →  (u : OD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
-         cx : {x : OD} →  ¬ (x == od∅ ) → choiced x 
+         Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
+         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
+         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced x 
          cx {x} nx = choice-func x nx
-         minimal : (x : OD  ) → ¬ (x == od∅ ) → OD 
-         minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) 
-         x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-         x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) 
-         minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+         minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD 
+         minimal x ne = min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) 
+         x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
+         x∋minimal x ne = x∋min (Min2 (a-choice (cx {x} ne) ) x (is-in (cx ne))) 
+         minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
          minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y
 
 
diff -r 9f926b2210bc -r ba3ebb9a16c6 OD.agda
--- a/OD.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/OD.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -53,28 +53,27 @@
 eq← ( ⇔→==  {x} {y}  eq ) {z} m = proj2 eq m 
 
 -- next assumptions are our axiom
---  it defines a subset of OD, which is called HOD, usually defined as
+--
+--  OD is an equation on Ordinals, so it contains Ordinals. If these Ordinals have one-to-one
+--  correspondence to the OD then the OD looks like a ZF Set.
+--
+--  If all ZF Set have supreme upper bound, the solutions of OD have to be bounded, i.e.
+--  bbounded ODs are ZF Set. Unbounded ODs are classes.
+--
+--  In classical Set Theory, HOD is used, as a subset of OD, 
 --     HOD = { x | TC x ⊆ OD }
---  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x
-
-record ODAxiom : Set (suc n) where      
-  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
- field
-  od→ord : OD  → Ordinal 
-  ord→od : Ordinal  → OD  
-  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
-  -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
-  sup-o  :  ( OD → Ordinal ) →  Ordinal 
-  sup-o< :  { ψ : OD →  Ordinal } → ∀ {x : OD } → ψ x  o<  sup-o ψ 
-  -- contra-position of mimimulity of supermum required in Power Set Axiom which we don't use
-  -- sup-x  : {n : Level } → ( OD → Ordinal ) →  Ordinal 
-  -- sup-lb : {n : Level } → { ψ : OD →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
-
-postulate  odAxiom : ODAxiom
-open ODAxiom odAxiom
+--  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x.
+--  This is not possible because we don't have V yet. So we assumes HODs are bounded OD.
+--
+--  We also assumes HODs are isomorphic to Ordinals, which is ususally proved by Goedel number tricks.
+--  There two contraints on the HOD order, one is ∋, the other one is ⊂.
+--  ODs have an ovbious maximum, but Ordinals are not, but HOD has no maximum because there is an aribtrary
+--  bound on each HOD.
+--
+--  In classical Set Theory, sup is defined by Uion, since we are working on constructive logic,
+--  we need explict assumption on sup.
+--
+--  ==→o≡ is necessary to prove axiom of extensionality.
 
 data One : Set n where
   OneObj : One
@@ -83,100 +82,125 @@
 Ords : OD
 Ords = record { def = λ x → One }
 
-maxod : {x : OD} → od→ord x o< od→ord Ords
-maxod {x} = c<→o< OneObj
+record HOD : Set (suc n) where
+  field
+    od : OD
+    odmax : Ordinal
+    <odmax : {y : Ordinal} → def od y → y o< odmax
+
+open HOD
+
+record ODAxiom : Set (suc n) where      
+ field
+  -- HOD is isomorphic to Ordinal (by means of Goedel number)
+  od→ord : HOD  → Ordinal 
+  ord→od : Ordinal  → HOD  
+  c<→o<  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y
+  ⊆→o≤  :   {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z)
+  oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
+  diso   :  {x : Ordinal }  → od→ord ( ord→od x ) ≡ x
+  ==→o≡ : { x y : HOD  }    → (od x == od y) → x ≡ y
+  sup-o  :  (A : HOD) → (( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal 
+  sup-o< :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o<  sup-o A ψ 
+
+postulate  odAxiom : ODAxiom
+open ODAxiom odAxiom
+
+-- maxod : {x : OD} → od→ord x o< od→ord Ords
+-- maxod {x} = c<→o< OneObj
+
+-- we have not this contradiction
+-- bad-bad : ⊥
+-- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One };  <odmax = {!!} } } OneObj)
 
 -- Ordinal in OD ( and ZFSet ) Transitive Set
-Ord : ( a : Ordinal  ) → OD 
-Ord  a = record { def = λ y → y o< a }  
+Ord : ( a : Ordinal  ) → HOD 
+Ord  a = record { od = record { def = λ y → y o< a } ; odmax = a ; <odmax = lemma } where
+   lemma :  {x : Ordinal} → x o< a → x o< a
+   lemma {x} lt = lt
+
+od∅ : HOD  
+od∅  = Ord o∅ 
 
-od∅ : OD  
-od∅  = Ord o∅ 
+odef : HOD → Ordinal → Set n
+odef A x = def ( od A ) x
+
+o<→c<→HOD=Ord : ( {x y : Ordinal  } → x o< y → odef (ord→od y) x ) → {x : HOD } →  x ≡ Ord (od→ord x)
+o<→c<→HOD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
+   lemma1 : {y : Ordinal} → odef x y → odef (Ord (od→ord x)) y
+   lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → odef x k ) (sym diso) lt))
+   lemma2 : {y : Ordinal} → odef (Ord (od→ord x)) y → odef x y
+   lemma2 {y} lt = subst (λ k → odef k y ) oiso (o<→c< {y} {od→ord x} lt )
 
 
-o<→c<→OD=Ord : ( {x y : Ordinal  } → x o< y → def (ord→od y) x ) → {x : OD } →  x ≡ Ord (od→ord x)
-o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
-   lemma1 : {y : Ordinal} → def x y → def (Ord (od→ord x)) y
-   lemma1 {y} lt = subst ( λ k → k o< od→ord x ) diso (c<→o< {ord→od y} {x} (subst (λ k → def x k ) (sym diso) lt))
-   lemma2 : {y : Ordinal} → def (Ord (od→ord x)) y → def x y
-   lemma2 {y} lt = subst (λ k → def k y ) oiso (o<→c< {y} {od→ord x} lt )
+_∋_ : ( a x : HOD  ) → Set n
+_∋_  a x  = odef a ( od→ord x )
 
-_∋_ : ( a x : OD  ) → Set n
-_∋_  a x  = def a ( od→ord x )
-
-_c<_ : ( x a : OD  ) → Set n
+_c<_ : ( x a : HOD  ) → Set n
 x c< a = a ∋ x 
 
-cseq : {n : Level} →  OD  →  OD 
-cseq x = record { def = λ y → def x (osuc y) } where
-
-def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
-def-subst df refl refl = df
+cseq : {n : Level} →  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)
+    lemma {y} lt = ordtrans <-osuc (ordtrans (<odmax x lt) <-osuc ) 
 
-sup-od : ( OD  → OD ) →  OD 
-sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ x)) )
+odef-subst :  {Z : HOD } {X : Ordinal  }{z : HOD } {x : Ordinal  }→ odef Z X → Z ≡ z  →  X ≡ x  →  odef z x
+odef-subst df refl refl = df
 
-sup-c< :  ( ψ : OD  →  OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x ))
-sup-c<   ψ {x} = def-subst  {_} {_} {Ord ( sup-o  ( λ x → od→ord (ψ x)) )} {od→ord ( ψ x )}
-        lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
-    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ x))
-    lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso)  )
-
-otrans : {n : Level} {a x y : Ordinal  } → def (Ord a) x → def (Ord x) y → def (Ord a) y
+otrans : {n : Level} {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
 otrans x<a y<x = ordtrans y<x x<a
 
-def→o< :  {X : OD } → {x : Ordinal } → def X x → x o< od→ord X 
-def→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( def-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso
-
+odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X 
+odef→o<  {X} {x} lt = o<-subst  {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst  {X} {x}  lt (sym oiso) (sym diso) )) diso diso
 
 -- avoiding lv != Zero error
-orefl : { x : OD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
+orefl : { x : HOD  } → { y : Ordinal  } → od→ord x ≡ y → od→ord x ≡ y
 orefl refl = refl
 
-==-iso : { x y : OD  } → ord→od (od→ord x) == ord→od (od→ord y)  →  x == y
+==-iso : { x y : HOD  } → od (ord→od (od→ord x)) == od (ord→od (od→ord y))  →  od x == od y
 ==-iso  {x} {y} eq = record {
-      eq→ = λ d →  lemma ( eq→  eq (def-subst d (sym oiso) refl )) ;
-      eq← = λ d →  lemma ( eq←  eq (def-subst d (sym oiso) refl ))  }
+      eq→ = λ d →  lemma ( eq→  eq (odef-subst d (sym oiso) refl )) ;
+      eq← = λ d →  lemma ( eq←  eq (odef-subst d (sym oiso) refl ))  }
         where
-           lemma : {x : OD  } {z : Ordinal } → def (ord→od (od→ord x)) z → def x z
-           lemma {x} {z} d = def-subst d oiso refl
+           lemma : {x : HOD  } {z : Ordinal } → odef (ord→od (od→ord x)) z → odef x z
+           lemma {x} {z} d = odef-subst d oiso refl
 
-=-iso :  {x y : OD  } → (x == y) ≡ (ord→od (od→ord x) == y)
-=-iso  {_} {y} = cong ( λ k → k == y ) (sym oiso)
+=-iso :  {x y : HOD  } → (od x == od y) ≡ (od (ord→od (od→ord x)) == od y)
+=-iso  {_} {y} = cong ( λ k → od k == od y ) (sym oiso)
 
-ord→== : { x y : OD  } → od→ord x ≡  od→ord y →  x == y
+ord→== : { x y : HOD  } → od→ord x ≡  od→ord y →  od x == od y
 ord→==  {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
-   lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
+   lemma : ( ox oy : Ordinal  ) → ox ≡ oy →  od (ord→od ox) == od (ord→od oy)
    lemma ox ox  refl = ==-refl
 
-o≡→== : { x y : Ordinal  } → x ≡  y →  ord→od x == ord→od y
+o≡→== : { x y : Ordinal  } → x ≡  y →  od (ord→od x) == od (ord→od y)
 o≡→==  {x} {.x} refl = ==-refl
 
 o∅≡od∅ : ord→od (o∅ ) ≡ od∅ 
 o∅≡od∅  = ==→o≡ lemma where
-     lemma0 :  {x : Ordinal} → def (ord→od o∅) x → def od∅ x
-     lemma0 {x} lt = o<-subst (c<→o<  {ord→od x} {ord→od o∅} (def-subst  {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
-     lemma1 :  {x : Ordinal} → def od∅ x → def (ord→od o∅) x
+     lemma0 :  {x : Ordinal} → odef (ord→od o∅) x → odef od∅ x
+     lemma0 {x} lt = o<-subst (c<→o<  {ord→od x} {ord→od o∅} (odef-subst  {ord→od o∅} {x} lt refl (sym diso)) ) diso diso
+     lemma1 :  {x : Ordinal} → odef od∅ x → odef (ord→od o∅) x
      lemma1 {x} lt = ⊥-elim (¬x<0 lt)
-     lemma : ord→od o∅ == od∅
+     lemma : od (ord→od o∅) == od od∅
      lemma = record { eq→ = lemma0 ; eq← = lemma1 }
 
 ord-od∅ : od→ord (od∅ ) ≡ o∅ 
 ord-od∅  = sym ( subst (λ k → k ≡  od→ord (od∅ ) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )
 
-∅0 : record { def = λ x →  Lift n ⊥ } == od∅  
+∅0 : record { def = λ x →  Lift n ⊥ } == od od∅  
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} lt = lift (¬x<0 lt)
 
-∅< : { x y : OD  } → def x (od→ord y ) → ¬ (  x  == od∅  )
+∅< : { x y : HOD  } → odef x (od→ord y ) → ¬ (  od x  == od od∅  )
 ∅<  {x} {y} d eq with eq→ (==-trans eq (==-sym ∅0) ) d
 ∅<  {x} {y} d eq | lift ()
        
-∅6 : { x : OD  }  → ¬ ( x ∋ x )    --  no Russel paradox
+∅6 : { x : HOD  }  → ¬ ( x ∋ x )    --  no Russel paradox
 ∅6  {x} x∋x = o<¬≡ refl ( c<→o<  {x} {x} x∋x )
 
-def-iso : {A B : OD } {x y : Ordinal } → x ≡ y  → (def A y → def B y)  → def A x → def B x
-def-iso refl t = t
+odef-iso : {A B : HOD } {x y : Ordinal } → x ≡ y  → (odef A y → odef B y)  → odef A x → odef B x
+odef-iso refl t = t
 
 is-o∅ : ( x : Ordinal  ) → Dec ( x ≡ o∅  )
 is-o∅ x with trio< x o∅
@@ -184,59 +208,72 @@
 is-o∅ x | tri≈ ¬a b ¬c = yes b
 is-o∅ x | tri> ¬a ¬b c = no ¬b
 
-_,_ : OD  → OD  → OD 
-x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } --  Ord (omax (od→ord x) (od→ord y))
+_,_ : HOD  → HOD  → HOD 
+x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = omax (od→ord x)  (od→ord y) ; <odmax = lemma }  where
+    lemma : {t : Ordinal} → (t ≡ od→ord x) ∨ (t ≡ od→ord y) → t o< omax (od→ord x) (od→ord y)
+    lemma {t} (case1 refl) = omax-x  _ _
+    lemma {t} (case2 refl) = omax-y  _ _
+
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
-in-codomain : (X : OD  ) → ( ψ : OD  → OD  ) → OD 
-in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
+in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD 
+in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
 
--- Power Set of X ( or constructible by λ y → def X (od→ord y )
-
-ZFSubset : (A x : OD  ) → OD 
-ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  --   roughly x = A → Set 
+-- Power Set of X ( or constructible by λ y → odef X (od→ord y )
 
-Def :  (A :  OD ) → OD 
-Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A x) ) )   
+ZFSubset : (A x : HOD  ) → HOD 
+ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma }  where --   roughly x = A → Set 
+     lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
+     lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
 
--- _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
--- _⊆_ A B {x} = A ∋ x →  B ∋ x
-
-record _⊆_ ( A B : OD   ) : Set (suc n) where
+record _⊆_ ( A B : HOD   ) : Set (suc n) where
   field 
-     incl : { x : OD } → A ∋ x →  B ∋ x
+     incl : { x : HOD } → A ∋ x →  B ∋ x
 
 open _⊆_
-
 infixr  220 _⊆_
 
-subset-lemma : {A x : OD  } → ( {y : OD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
+subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
 subset-lemma  {A} {x} = record {
       proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
     ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 
    } 
 
+od⊆→o≤  : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
+od⊆→o≤ {x} {y} lt  =  ⊆→o≤ {x} {y} (λ {z} x>z  → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z )))
+
+power< : {A x : HOD  } → x ⊆ A → Ord (osuc (od→ord A)) ∋ x
+power< {A} {x} x⊆A = ⊆→o≤  (λ {y} x∋y → subst (λ k →  def (od A) k) diso (lemma y x∋y ) ) where
+    lemma : (y : Ordinal) → def (od x) y → def (od A) (od→ord (ord→od y))
+    lemma y x∋y = incl x⊆A (subst (λ k → def (od x) k ) (sym diso) x∋y )
+
 open import Data.Unit
 
-ε-induction : { ψ : OD  → Set (suc n)}
-   → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
-   → (x : OD ) → ψ x
+ε-induction : { ψ : HOD  → Set n}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
 ε-induction {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
      induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
      induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
--- minimal-2 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
--- minimal-2 x ne y = contra-position ( ε-induction (λ {z} ind → {!!} ) x ) ( λ p → {!!} )
+ε-induction1 : { ψ : HOD  → Set (suc n)}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
+ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
 
-OD→ZF : ZF  
-OD→ZF   = record { 
-    ZFSet = OD 
+HOD→ZF : ZF  
+HOD→ZF   = record { 
+    ZFSet = HOD 
     ; _∋_ = _∋_ 
-    ; _≈_ = _==_ 
+    ; _≈_ = _=h=_ 
     ; ∅  = od∅
     ; _,_ = _,_
     ; Union = Union
@@ -246,19 +283,43 @@
     ; infinite = infinite
     ; isZF = isZF 
  } where
-    ZFSet = OD             -- is less than Ords because of maxod
-    Select : (X : OD  ) → ((x : OD  ) → Set n ) → OD 
-    Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
-    Replace : OD  → (OD  → OD  ) → OD 
-    Replace X ψ = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x }
+    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
     _∩_ : ( A B : ZFSet  ) → ZFSet
-    A ∩ B = record { def = λ x → def A x ∧ def B x } 
-    Union : OD  → OD   
-    Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
+    A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x }
+        ; odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y))}
+    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
-    Power : OD  → OD 
-    Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
+
+    OPwr :  (A :  HOD ) → HOD 
+    OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )   
+
+    Power : HOD  → HOD 
+    Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
     -- ｛_｝ : ZFSet → ZFSet
     -- ｛ x ｝ = ( x ,  x )     -- it works but we don't use 
 
@@ -267,12 +328,25 @@
         isuc : {x : Ordinal  } →   infinite-d  x  →
                 infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
 
-    infinite : OD 
-    infinite = record { def = λ x → infinite-d x }
+    -- ω can be diverged in our case, since we have no restriction on the corresponding ordinal of a pair.
+    -- We simply assumes nfinite-d y has a maximum.
+    -- 
+    -- This means that many of OD cannot be HODs because of the od→ord mapping divergence.
+    -- We should have some axioms to prevent this, but it may complicate thins.
+    -- 
+    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 } 
+
+    _=h=_ : (x y : HOD) → Set n
+    x =h= y  = od x == od y
 
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZF : IsZF (OD )  _∋_  _==_ od∅ _,_ Union Power Select Replace infinite
+    isZF : IsZF (HOD )  _∋_  _=h=_ od∅ _,_ Union Power Select Replace infinite
     isZF = record {
            isEquivalence  = record { refl = ==-refl ; sym = ==-sym; trans = ==-trans }
        ;   pair→  = pair→
@@ -288,20 +362,20 @@
        ;   infinity = infinity
        ;   selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
        ;   replacement← = replacement←
-       ;   replacement→ = replacement→
+       ;   replacement→ = λ {ψ} → replacement→ {ψ}
        -- ;   choice-func = choice-func
        -- ;   choice = choice
      } where
 
-         pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y ) 
-         pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x ))
-         pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y ))
+         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 == x ) ∨ ( t == y ) →  (x , y)  ∋ t  
-         pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
-         pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→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 : OD  ) → ¬  (od∅ ∋ x)
+         empty : (x : HOD  ) → ¬  (od∅ ∋ x)
          empty x = ¬x<0 
 
          o<→c< :  {x y : Ordinal } → x o< y → (Ord x) ⊆ (Ord y) 
@@ -314,114 +388,167 @@
          ⊆→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 : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         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 → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
-         union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+              ; 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} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
-              lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx } 
+              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 :  {ψ : OD  → Set n} {x y : OD } → ψ x → x ≡ y   → ψ y
+         ψiso :  {ψ : HOD  → Set n} {x y : HOD } → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
-         selection : {ψ : OD → Set n} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
+         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  }
            }
-         replacement← : {ψ : OD → OD} (X x : OD) →  X ∋ x → Replace X ψ ∋ ψ x
-         replacement← {ψ} X x lt = record { proj1 =  sup-c< ψ {x} ; proj2 = lemma } where
+         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→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → ¬ ( (y : OD) → ¬ (x == ψ y))
+         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) → ¬ def X y ∧ ((od→ord x) ≡ od→ord (ψ (ord→od y))))
-                    → ¬ ((y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)))
+            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) == ψ (ord→od y))  
-                lemma3 {y} eq = subst (λ k  → ord→od (od→ord x) == k ) oiso (o≡→== eq )
-            lemma :  ( (y : OD) → ¬ (x == ψ y)) → ( (y : Ordinal) → ¬ def X y ∧ (ord→od (od→ord x) == ψ (ord→od y)) )
-            lemma not y not2 = not (ord→od y) (subst (λ k → k == ψ (ord→od y)) oiso  ( proj2 not2 ))
+                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 OD
+         ---    First consider ordinals in HOD
          ---
-         --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
+         --- ZFSubset A x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
          --
          --
-         ∩-≡ :  { a b : OD  } → ({x : OD  } → (a ∋ x → b ∋ x)) → a == ( b ∩ 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 = def-subst  {_} {_} {b} {x} (inc (def-subst  {_} {_} {a} {_} x<a refl (sym diso) )) refl diso  } ;
+                 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 ZFSubset (Ord a) t == t
-         -- Def (Ord a) is a sup of ZFSubset (Ord a) t, so Def (Ord a) ∋ t
-         -- Def  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+         -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t =h= t
+         -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t
+         -- OPwr  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
          -- 
-         ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
-         ord-power← a t t→A  = def-subst  {_} {_} {Def (Ord a)} {od→ord t}
+         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 :  ZFSubset (Ord a) t == t
+              lemma-eq :  ZFSubset (Ord a) t =h= t
               eq→ lemma-eq {z} w = proj2 w 
               eq← lemma-eq {z} w = record { proj2 = w  ;
-                 proj1 = def-subst  {_} {_} {(Ord a)} {z}
-                    ( t→A (def-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
-              lemma1 :  {a : Ordinal } { t : OD }
-                 → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
+                 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 : ZFSubset (Ord a) t =h= t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
               lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o  (λ x → od→ord (ZFSubset (Ord a) x))
-              lemma = sup-o<  
+              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 (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma = sup-o< _ lemma2
 
          -- 
-         -- Every set in OD is a subset of Ordinals, so make Def (Ord (od→ord A)) first
+         -- 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 (Def (Ord (od→ord A))) ( λ y → 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 : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+         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 : OD) → ¬ (t ==  (A ∩ y)))
-              lemma2 = replacement→ (Def (Ord (od→ord A))) t P∋t
-              lemma3 : (y : OD) → t == ( A ∩ y ) → ¬ ¬ (A ∋ x)
+              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 == (A ∩ ord→od y)))
-              lemma4 not = lemma2 ( λ y not1 → not (od→ord y) (subst (λ k → t == ( A ∩ k )) (sym oiso) not1 ))
-              lemma5 : {y : Ordinal} → t == (A ∩ ord→od y) →  ¬ ¬  (def A (od→ord 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 : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+         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 : OD} → t ∋ x → Ord a ∋ x
+              lemma0 : {x : HOD} → t ∋ x → Ord a ∋ x
               lemma0 {x} t∋x = c<→o< (t→A t∋x)
-              lemma3 : Def (Ord a) ∋ t
+              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 )) ⟩
+                 ≡⟨ sym (==→o≡ ( ∩-≡ {t} {A} t→A )) ⟩
                     t
                  ∎
-              lemma1 : od→ord t o< sup-o  (λ x → od→ord (A ∩ x))
-              lemma1 = subst (λ k → od→ord k o< sup-o   (λ x → od→ord (A ∩ x)))
-                  lemma4 (sup-o<  {λ x → od→ord (A ∩ x)}  )
-              lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
+              sup1 : Ordinal
+              sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (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 (ZFSubset (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 : ZFSubset (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 (ZFSubset (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 (ZFSubset (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 (ZFSubset (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 == (A ∩ k)) (sym oiso) ( ∩-≡ t→A  )))
+                  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 : OD} → od→ord x o< osuc a → x ∋ y →  Ord a ∋ y
+                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 
@@ -429,16 +556,16 @@
          continuum-hyphotheis : (a : Ordinal) → Set (suc n)
          continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)
 
-         extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
-         eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso  {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
-         eq← (extensionality0 {A} {B} eq ) {x} d = def-iso  {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
+         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 : OD  } → ((z : OD ) → (A ∋ z) ⇔ (B ∋ z)) → (w ∋ A) ⇔ (w ∋ B)
+         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∅ = def-subst  {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
+         infinity∅ = odef-subst  {_} {_} {infinite} {od→ord (od∅ )} iφ refl lemma where
               lemma : o∅ ≡ od→ord od∅
               lemma =  let open ≡-Reasoning in begin
                     o∅
@@ -447,15 +574,15 @@
                  ≡⟨ cong ( λ k → od→ord k ) o∅≡od∅ ⟩
                     od→ord od∅
                  ∎
-         infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
-         infinity x lt = def-subst  {_} {_} {infinite} {od→ord (Union (x , (x , x )))} ( isuc {od→ord x} lt ) refl lemma where
+         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 OD→ZF
-Power = ZF.Power OD→ZF
-Select = ZF.Select OD→ZF
-Replace = ZF.Replace OD→ZF
-isZF = ZF.isZF  OD→ZF
+Union = ZF.Union HOD→ZF
+Power = ZF.Power HOD→ZF
+Select = ZF.Select HOD→ZF
+Replace = ZF.Replace HOD→ZF
+isZF = ZF.isZF  HOD→ZF
diff -r 9f926b2210bc -r ba3ebb9a16c6 ODC.agda
--- a/ODC.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/ODC.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -21,13 +21,20 @@
 open OD._==_
 open ODAxiom odAxiom
 
+open HOD
+
+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 : OD  ) → ¬ (x == od∅ )→ OD 
-  -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
-  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-  -- minimality (may proved by ε-induction )
-  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+  minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
+  -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
+  x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
+  -- minimality (may proved by ε-induction with LEM)
+  minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
 
 
 --
@@ -35,20 +42,26 @@
 --     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
 --
 
-ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
-ppp  {p} {a} d = d
+pred-od :  ( p : Set n )  → HOD
+pred-od  p  = record { od = record { def = λ x → (x ≡ o∅) ∧ p } ;
+   odmax = osuc o∅; <odmax = λ x → subst (λ k →  k o< osuc o∅) (sym (proj1 x)) <-osuc } 
+
+ppp :  { p : Set n } { a : HOD  } → pred-od p ∋ a → p
+ppp  {p} {a} d = proj2 d
 
 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
-p∨¬p  p with is-o∅ ( od→ord ( record { def = λ x → p } ))
+p∨¬p  p with is-o∅ ( od→ord (pred-od p ))
 p∨¬p  p | yes eq = case2 (¬p eq) where
-   ps = record { def = λ x → p }
-   lemma : ps == od∅ → p → ⊥
-   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq p0 )
+   ps = pred-od p 
+   eqo∅ : ps =h=  od∅  → od→ord ps ≡  o∅  
+   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
+   lemma : ps =h= od∅ → p → ⊥
+   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq record { proj1 = eqo∅ eq ; proj2 = p0 } )
    ¬p : (od→ord ps ≡ o∅) → p → ⊥
-   ¬p eq = lemma ( subst₂ (λ j k → j ==  k ) oiso o∅≡od∅ ( o≡→== eq ))
+   ¬p eq = lemma ( subst₂ (λ j k → j =h=  k ) oiso o∅≡od∅ ( o≡→== eq ))
 p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
-   ps = record { def = λ x → p }
-   eqo∅ : ps ==  od∅  → od→ord ps ≡  o∅  
+   ps = pred-od p 
+   eqo∅ : ps =h=  od∅  → od→ord ps ≡  o∅  
    eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
    lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
    lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
@@ -63,7 +76,7 @@
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
-OrdP : ( x : Ordinal  ) ( y : OD  ) → Dec ( Ord x ∋ y )
+OrdP : ( x : Ordinal  ) ( y : HOD  ) → Dec ( Ord x ∋ y )
 OrdP  x y with trio< x (od→ord y)
 OrdP  x y | tri< a ¬b ¬c = no ¬c
 OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
@@ -71,26 +84,26 @@
 
 open import zfc
 
-OD→ZFC : ZFC
-OD→ZFC   = record { 
-    ZFSet = OD 
+HOD→ZFC : ZFC
+HOD→ZFC   = record { 
+    ZFSet = HOD 
     ; _∋_ = _∋_ 
-    ; _≈_ = _==_ 
+    ; _≈_ = _=h=_ 
     ; ∅  = od∅
     ; Select = Select
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select 
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ od∅ Select 
     isZFC = record {
        choice-func = choice-func ;
        choice = choice
      } where
          -- Axiom of choice ( is equivalent to the existence of minimal in our case )
          -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
-         choice-func : (X : OD  ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
+         choice-func : (X : HOD  ) → {x : HOD } → ¬ ( x =h= od∅ ) → ( X ∋ x ) → HOD
          choice-func X {x} not X∋x = minimal x not
-         choice : (X : OD  ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
+         choice : (X : HOD  ) → {A : HOD } → ( X∋A : X ∋ A ) → (not : ¬ ( A =h= od∅ )) → A ∋ choice-func X not X∋A 
          choice X {A} X∋A not = x∋minimal A not
 
diff -r 9f926b2210bc -r ba3ebb9a16c6 OPair.agda
--- a/OPair.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/OPair.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -17,6 +17,7 @@
 open inOrdinal O
 open OD O
 open OD.OD
+open OD.HOD
 open ODAxiom odAxiom
 
 open _∧_
@@ -25,30 +26,33 @@
 
 open _==_
 
-<_,_> : (x y : OD) → OD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
+<_,_> : (x y : HOD) → HOD
 < x , y > = (x , x ) , (x , y )
 
-exg-pair : { x y : OD } → (x , y ) == ( y , x )
+exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
-    left : {z : Ordinal} → def (x , y) z → def (y , x) z 
+    left : {z : Ordinal} → odef (x , y) z → odef (y , x) z 
     left (case1 t) = case2 t
     left (case2 t) = case1 t
-    right : {z : Ordinal} → def (y , x) z → def (x , y) z 
+    right : {z : Ordinal} → odef (y , x) z → odef (x , y) z 
     right (case1 t) = case2 t
     right (case2 t) = case1 t
 
-ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y
+ord≡→≡ : { x y : HOD } → od→ord x ≡ od→ord y → x ≡ y
 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq )
 
 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y
 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq )
 
-eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
 eq-prod refl refl = refl
 
-prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
 prod-eq {x} {x'} {y} {y'} eq = record { proj1 = lemmax ; proj2 = lemmay } where
-    lemma0 : {x y z : OD } → ( x , x ) == ( z , y ) → x ≡ y
+    lemma0 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
     lemma0 {x} {y} eq with trio< (od→ord x) (od→ord y) 
     lemma0 {x} {y} eq | tri< a ¬b ¬c with eq← eq {od→ord y} (case2 refl) 
     lemma0 {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
@@ -57,15 +61,15 @@
     lemma0 {x} {y} eq | tri> ¬a ¬b c  with eq← eq {od→ord y} (case2 refl) 
     lemma0 {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
     lemma0 {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
-    lemma2 : {x y z : OD } → ( x , x ) == ( z , y ) → z ≡ y
+    lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
     lemma2 {x} {y} {z} eq = trans (sym (lemma0 lemma3 )) ( lemma0 eq )  where
-        lemma3 : ( x , x ) == ( y , z )
+        lemma3 : ( x , x ) =h= ( y , z )
         lemma3 = ==-trans eq exg-pair
-    lemma1 : {x y : OD } → ( x , x ) == ( y , y ) → x ≡ y
+    lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
     lemma1 {x} {y} eq with eq← eq {od→ord y} (case2 refl)
     lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
     lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
-    lemma4 : {x y z : OD } → ( x , y ) == ( x , z ) → y ≡ z
+    lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
     lemma4 {x} {y} {z} eq with eq← eq {od→ord z} (case2 refl)
     lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
     ... | refl with lemma2 (==-sym eq )
@@ -81,6 +85,9 @@
     ... | refl with lemma4 eq -- with (x,y)≡(x,y')
     ... | eq1 = lemma4 (ord→== (cong (λ  k → od→ord k )  eq1 ))
 
+--
+-- unlike ordered pair, ZFProduct is not a HOD
+
 data ord-pair : (p : Ordinal) → Set n where
    pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
 
@@ -94,35 +101,38 @@
 pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
 pi1 ( pair x y) = x
 
-π1 : { p : OD } → ZFProduct ∋ p → OD
+π1 : { p : HOD } → def ZFProduct (od→ord p) → HOD
 π1 lt = ord→od (pi1 lt )
 
 pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
 pi2 ( pair x y ) = y
 
-π2 : { p : OD } → ZFProduct ∋ p → OD
+π2 : { p : HOD } → def ZFProduct (od→ord p) → HOD
 π2 lt = ord→od (pi2 lt )
 
-op-cons :  { ox oy  : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >  
+op-cons :  { ox oy  : Ordinal } → def ZFProduct (od→ord ( < ord→od ox , ord→od oy >   ))
 op-cons {ox} {oy} = pair ox oy
 
-p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
-p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
-    let open ≡-Reasoning in begin
-        od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
-    ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
-        od→ord < x , y >
-    ∎ ) 
+def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
+def-subst df refl refl = df
+
+p-cons :  ( x y  : HOD ) → def ZFProduct (od→ord ( < x , y >))
+p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
+   let open ≡-Reasoning in begin
+       od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
+   ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
+       od→ord < x , y >
+   ∎ ) 
 
 op-iso :  { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
 op-iso (pair ox oy) = refl
 
-p-iso :  { x  : OD } → (p : ZFProduct ∋ x ) → < π1 p , π2 p > ≡ x
+p-iso :  { x  : HOD } → (p : def ZFProduct (od→ord  x) ) → < π1 p , π2 p > ≡ x
 p-iso {x} p = ord≡→≡ (op-iso p) 
 
-p-pi1 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π1 p ≡ x
+p-pi1 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π1 p ≡ x
 p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
 
-p-pi2 :  { x y : OD } → (p : ZFProduct ∋ < x , y > ) →  π2 p ≡ y
+p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
diff -r 9f926b2210bc -r ba3ebb9a16c6 Ordinals.agda
--- a/Ordinals.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/Ordinals.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -13,14 +13,19 @@
 open import Relation.Binary
 open import Relation.Binary.Core
 
-record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
+record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
    field
      Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
      OTri : Trichotomous {n} _≡_  _o<_ 
      ¬x<0 :   { x  : ord  } → ¬ ( x o< o∅  )
      <-osuc :  { x : ord  } → x o< osuc x
      osuc-≡< :  { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)  
-     TransFinite : { ψ : ord  → Set (suc n) }
+     not-limit :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
+     next-limit : { y : ord } → (y o< next y ) ∧  ((x : ord) → x o< next y → osuc x o< next y )
+     TransFinite : { ψ : ord  → Set n }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
+     TransFinite1 : { ψ : ord  → Set (suc n) }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
 
@@ -31,7 +36,8 @@
      o∅ : ord
      osuc : ord → ord
      _o<_ : ord → ord → Set n
-     isOrdinal : IsOrdinals ord o∅ osuc _o<_
+     next :  ord → ord
+     isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
 
 module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
@@ -47,11 +53,16 @@
         o∅ :   Ordinal  
         o∅ = Ordinals.o∅ O
 
+        next :   Ordinal → Ordinal
+        next = Ordinals.next O
+
         ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
         osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
-        
+        TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
+        next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)
+
         o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
         o<-dom  {x} _ = x
 
@@ -104,7 +115,7 @@
         proj1 (osuc2 x y) ox<ooy | case2 ox<oy = ordtrans <-osuc ox<oy 
 
         _o≤_ :  Ordinal → Ordinal → Set  n
-        a o≤ b  = (a ≡ b)  ∨ ( a o< b )
+        a o≤ b  = a o< osuc b -- (a ≡ b)  ∨ ( a o< b )
 
 
         xo<ab :  {oa ob : Ordinal } → ( {ox : Ordinal } → ox o< oa  → ox o< ob ) → oa o< osuc ob
@@ -119,13 +130,13 @@
         maxα x y | tri> ¬a ¬b c = x
         maxα x y | tri≈ ¬a refl ¬c = x
 
-        minα :    Ordinal  →  Ordinal  → Ordinal
-        minα  x y with trio<  x  y
-        minα x y | tri< a ¬b ¬c = x
-        minα x y | tri> ¬a ¬b c = y
-        minα x y | tri≈ ¬a refl ¬c = x
+        omin :    Ordinal  →  Ordinal  → Ordinal
+        omin  x y with trio<  x  y
+        omin x y | tri< a ¬b ¬c = x
+        omin x y | tri> ¬a ¬b c = y
+        omin x y | tri≈ ¬a refl ¬c = x
 
-        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< minα x y
+        min1 :   {x y z : Ordinal  } → z o< x → z o< y → z o< omin x y
         min1  {x} {y} {z} z<x z<y with trio<  x y
         min1  {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
         min1  {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
@@ -176,11 +187,14 @@
 
         open _∧_
 
+        o≤-refl :  { i  j : Ordinal } → i ≡ j → i o≤ j
+        o≤-refl {i} {j} eq = subst (λ k → i o< osuc k ) eq <-osuc
         OrdTrans :  Transitive  _o≤_
-        OrdTrans (case1 refl) (case1 refl) = case1 refl
-        OrdTrans (case1 refl) (case2 lt2) = case2 lt2
-        OrdTrans (case2 lt1) (case1 refl) = case2 lt1
-        OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
+        OrdTrans a≤b b≤c with osuc-≡< a≤b | osuc-≡< b≤c
+        OrdTrans a≤b b≤c | case1 refl | case1 refl = <-osuc
+        OrdTrans a≤b b≤c | case1 refl | case2 a≤c = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a≤c | case1 refl = ordtrans a≤c <-osuc
+        OrdTrans a≤b b≤c | case2 a<b | case2 b<c = ordtrans (ordtrans a<b  b<c) <-osuc
 
         OrdPreorder :   Preorder n n n
         OrdPreorder  = record { Carrier = Ordinal
@@ -188,7 +202,7 @@
            ; _∼_   = _o≤_
            ; isPreorder   = record {
                 isEquivalence = record { refl = refl  ; sym = sym ; trans = trans }
-                ; reflexive     = case1 
+                ; reflexive     = o≤-refl
                 ; trans         = OrdTrans 
              }
          }
@@ -199,3 +213,11 @@
           → ¬ p
         FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
+        record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
+          field
+            os→ : (x : Ordinal) → x o< maxordinal → Ordinal
+            os← : Ordinal → Ordinal
+            os←limit : (x : Ordinal) → os← x o< maxordinal
+            os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
+            os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
+
diff -r 9f926b2210bc -r ba3ebb9a16c6 cardinal.agda
--- a/cardinal.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/cardinal.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -29,49 +29,48 @@
 -- we have to work on Ordinal to keep OD Level n
 -- since we use p∨¬p which works only on Level n
 
-    
-∋-p : (A x : OD ) → Dec ( A ∋ x ) 
+∋-p : (A x : HOD ) → Dec ( A ∋ x ) 
 ∋-p A x with ODC.p∨¬p O ( A ∋ x )
 ∋-p A x | case1 t = yes t
 ∋-p A x | case2 t = no t
 
-_⊗_  : (A B : OD) → OD
-A ⊗ B  = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where
+_⊗_  : (A B : HOD) → HOD
+A ⊗ B  = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } } where
     checkAB : { p : Ordinal } → def ZFProduct p → Set n
-    checkAB (pair x y) = def A x ∧ def B y
+    checkAB (pair x y) = odef A x ∧ odef B y
 
-func→od0  : (f : Ordinal → Ordinal ) → OD
-func→od0  f = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) } where
+func→od0  : (f : Ordinal → Ordinal ) → HOD
+func→od0  f = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) }}  where
     checkfunc : { p : Ordinal } → def ZFProduct p → Set n
     checkfunc (pair x y) = f x ≡ y
 
 --  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
 
-Func :  ( A B : OD ) → OD
-Func A B = record { def = λ x → def (Power (A ⊗ B)) x } 
+Func :  ( A B : HOD ) → HOD
+Func A B = record { od = record { def = λ x → odef (Power (A ⊗ B)) x }  }
 
 -- power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
 
-func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
+func→od : (f : Ordinal → Ordinal ) → ( dom : HOD ) → HOD 
 func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
 
-record Func←cd { dom cod : OD } {f : Ordinal }  : Set n where
+record Func←cd { dom cod : HOD } {f : Ordinal }  : Set n where
    field
       func-1 : Ordinal → Ordinal
       func→od∈Func-1 :  Func dom cod ∋  func→od func-1 dom
  
-od→func : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f  → Func←cd {dom} {cod} {f} 
-od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
+od→func : { dom cod : HOD } → {f : Ordinal }  → odef (Func dom cod ) f  → Func←cd {dom} {cod} {f} 
+od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o {!!} ( λ y lt → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
    lemma : Ordinal → Ordinal → Ordinal
-   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → odef (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
    lemma x y | p | no n  = o∅
    lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
            lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
            lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
            lemma2 (pair x1 y1) | yes p = y1
            lemma2 (pair x1 y1) | no ¬p = o∅
-   fod : OD
-   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > )
+   fod : HOD
+   fod = Replace dom ( λ x →  < x , ord→od (sup-o {!!} ( λ y lt → lemma (od→ord x) {!!} )) > )
 
 
 open Func←cd
@@ -91,18 +90,18 @@
 --     X ---------------------------> Y
 --          ymap   <-  def Y y
 --
-record Onto  (X Y : OD )  : Set n where
+record Onto  (X Y : HOD )  : Set n where
    field
        xmap : Ordinal 
        ymap : Ordinal 
-       xfunc : def (Func X Y) xmap 
-       yfunc : def (Func Y X) ymap 
-       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) →
+       xfunc : odef (Func X Y) xmap 
+       yfunc : odef (Func Y X) ymap 
+       onto-iso   : {y :  Ordinal  } → (lty : odef Y y ) →
           func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func  yfunc) y )  ≡ y 
 
 open Onto
 
-onto-restrict : {X Y Z : OD} → Onto X Y → Z ⊆ Y  → Onto X Z
+onto-restrict : {X Y Z : HOD} → Onto X Y → Z ⊆ Y  → Onto X Z
 onto-restrict {X} {Y} {Z} onto  Z⊆Y = record {
      xmap = xmap1
    ; ymap = zmap
@@ -114,23 +113,23 @@
        xmap1 = od→ord (Select (ord→od (xmap onto)) {!!} ) 
        zmap : Ordinal 
        zmap = {!!}
-       xfunc1 : def (Func X Z) xmap1
+       xfunc1 : odef (Func X Z) xmap1
        xfunc1 = {!!}
-       zfunc : def (Func Z X) zmap 
+       zfunc : odef (Func Z X) zmap 
        zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func-1 (od→func  xfunc1 )  (func-1 (od→func  zfunc ) z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : odef Z z ) → func-1 (od→func  xfunc1 )  (func-1 (od→func  zfunc ) z )  ≡ z
        onto-iso1   = {!!}
 
 
-record Cardinal  (X  : OD ) : Set n where
+record Cardinal  (X  : HOD ) : Set n where
    field
        cardinal : Ordinal 
        conto : Onto X (Ord cardinal)  
        cmax : ( y : Ordinal  ) → cardinal o< y → ¬ Onto X (Ord y)  
 
-cardinal :  (X  : OD ) → Cardinal X
+cardinal :  (X  : HOD ) → Cardinal X
 cardinal  X = record {
-       cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) )
+       cardinal = sup-o {!!} ( λ x lt → proj1 ( cardinal-p {!!}) )
      ; conto = onto
      ; cmax = cmax
    } where
@@ -138,24 +137,24 @@
     cardinal-p x with ODC.p∨¬p O ( Onto X (Ord x)  ) 
     cardinal-p x | case1 True  = record { proj1 = x  ; proj2 = yes True }
     cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
-    S = sup-o (λ x → proj1 (cardinal-p {!!}))
-    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) →
-                    Lift (suc n) (x o< (osuc S) → Onto X (Ord x) )
+    S = sup-o {!!} (λ x lt → proj1 (cardinal-p {!!}))
+    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x →  (y o< (osuc S) → Onto X (Ord y))) →
+                     (x o< (osuc S) → Onto X (Ord x) )
     lemma1 x prev with trio< x (osuc S)
     lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a
-    lemma1 x prev | tri< a ¬b ¬c | case1 x=S = lift ( λ lt → {!!} )
-    lemma1 x prev | tri< a ¬b ¬c | case2 x<S = lift ( λ lt → lemma2 ) where
+    lemma1 x prev | tri< a ¬b ¬c | case1 x=S = ( λ lt → {!!} )
+    lemma1 x prev | tri< a ¬b ¬c | case2 x<S = ( λ lt → lemma2 ) where
          lemma2 : Onto X (Ord x) 
          lemma2 with prev {!!} {!!}
-         ... | lift t = t {!!}
-    lemma1 x prev | tri≈ ¬a b ¬c = lift ( λ lt → ⊥-elim ( o<¬≡ b lt ))
-    lemma1 x prev | tri> ¬a ¬b c = lift ( λ lt → ⊥-elim ( o<> c lt ))
+         ... | t = {!!}
+    lemma1 x prev | tri≈ ¬a b ¬c = ( λ lt → ⊥-elim ( o<¬≡ b lt ))
+    lemma1 x prev | tri> ¬a ¬b c = ( λ lt → ⊥-elim ( o<> c lt ))
     onto : Onto X (Ord S) 
-    onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto X (Ord x) ) } lemma1 S 
-    ... | lift t = t <-osuc  
+    onto with TransFinite {λ x →  ( x o< osuc S → Onto X (Ord x) ) } lemma1 S 
+    ... | t = t <-osuc  
     cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y) 
-    cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S}
-       (sup-o<  {λ x → proj1 ( cardinal-p {!!})}{{!!}}  ) lemma refl ) where
+    cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S} {!!} lemma refl ) where
+       -- (sup-o<  ? {λ x lt → proj1 ( cardinal-p {!!})}{{!!}}  ) lemma refl ) where
           lemma : proj1 (cardinal-p y) ≡ y
           lemma with  ODC.p∨¬p O ( Onto X (Ord y) )
           lemma | case1 x = refl
diff -r 9f926b2210bc -r ba3ebb9a16c6 filter.agda
--- a/filter.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/filter.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -13,80 +13,143 @@
 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 BAlgbra
+
+open BAlgbra O
 
 open inOrdinal O
 open OD O
 open OD.OD
 open ODAxiom odAxiom
 
+import ODC
+
 open _∧_
 open _∨_
 open Bool
 
-_∩_ : ( A B : OD  ) → OD
-A ∩ B = record { def = λ x → def A x ∧ def B x } 
-
-_∪_ : ( A B : OD  ) → OD
-A ∪ B = record { def = λ x → def A x ∨ def B x } 
-
-_＼_ : ( A B : OD  ) → OD
-A ＼ B = record { def = λ x → def A x ∧ ( ¬ ( def B x ) ) }
-
-
-record Filter  ( L : OD  ) : Set (suc n) where
+-- Kunen p.76 and p.53, we use ⊆
+record Filter  ( L : HOD  ) : Set (suc n) where
    field
-       filter : OD
-       proper : ¬ ( filter ∋ od∅ )
-       inL :  filter ⊆ L 
-       filter1 : { p q : OD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
-       filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
+       filter : HOD   
+       f⊆PL :  filter ⊆ Power L 
+       filter1 : { p q : HOD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+       filter2 : { p q : HOD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
 
 open Filter
 
-L⊆L : (L : OD) → L ⊆ L
-L⊆L L = record { incl = λ {x} lt → lt }
+record prime-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
+   field
+       proper  : ¬ (filter P ∋ od∅)
+       prime   : {p q : HOD } →  filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+
+record ultra-filter { L : HOD } (P : Filter L) : Set (suc (suc n)) where
+   field
+       proper  : ¬ (filter P ∋ od∅)
+       ultra   : {p : HOD } → p ⊆ L →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
 
-L-filter : {L : OD} → (P : Filter L ) → {p : OD} → filter P ∋ p → filter P ∋ L
-L-filter {L} P {p} lt = filter1 P {p} {L} (L⊆L L) lt {!!}
+open _⊆_
+
+trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
+trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
 
-prime-filter : {L : OD} → Filter L → ∀ {p q : OD } → Set n
-prime-filter {L} P {p} {q} =  filter P ∋ ( p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+power→⊆ :  ( A t : HOD) → Power A ∋ t → t ⊆ A
+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
 
-ultra-filter :  {L : OD} → Filter L → ∀ {p : OD } → Set n 
-ultra-filter {L} P {p} = L ∋ p →  ( filter P ∋ p ) ∨ (  filter P ∋ ( L ＼ p) )
+∈-filter : {L p : HOD} → (P : Filter L ) → filter P ∋ p → p ⊆ L
+∈-filter {L} {p} P lt = power→⊆ L p ( incl (f⊆PL P) lt )
 
+∪-lemma1 : {L p q : HOD } → (p ∪ q)  ⊆ L → p ⊆ L
+∪-lemma1 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case1 p∋x) }
+
+∪-lemma2 : {L p q : HOD } → (p ∪ q)  ⊆ L → q ⊆ L
+∪-lemma2 {L} {p} {q} lt = record { incl = λ {x} p∋x → incl lt (case2 p∋x) }
 
-filter-lemma1 :  {L : OD} → (P : Filter L)  → ∀ {p q : OD } → ( ∀ (p : OD ) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
-filter-lemma1 {L} P {p} {q} u lt = {!!}
+q∩q⊆q : {p q : HOD } → (q ∩ p) ⊆ q 
+q∩q⊆q = record { incl = λ lt → proj1 lt } 
 
-filter-lemma2 :  {L : OD} → (P : Filter L)  → ( ∀ {p q : OD } → prime-filter {L} P {p} {q}) →  ∀ (p : OD ) → ultra-filter {L} P {p} 
-filter-lemma2 {L} P prime p with prime {!!}
-... | t = {!!}
+open HOD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
+-----
+--
+--  ultra filter is prime
+--
 
-generated-filter : {L : OD} → Filter L → (p : OD ) → Filter ( record { def = λ x → def L x ∨ (x ≡ od→ord p) } )
-generated-filter {L} P p = record {
-     proper = {!!} ; 
-     filter = {!!}  ; inL = {!!} ; 
-     filter1 = {!!} ; filter2 = {!!}
-   }
+filter-lemma1 :  {L : HOD} → (P : Filter L)  → ∀ {p q : HOD } → ultra-filter P  → prime-filter P 
+filter-lemma1 {L} P u = record {
+         proper = ultra-filter.proper u
+       ; prime = lemma3
+    } where
+  lemma3 : {p q : HOD} → filter P ∋ (p ∪ q) → ( filter P ∋ p ) ∨ ( filter P ∋ q )
+  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)) =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 ) → 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
+    lemma6 : filter P ∋ ((p ∪ q ) ∩ (L ＼ p))
+    lemma6 = filter2 P lt ¬p∈P
+    lemma7 : filter P ∋ (q ∩ (L ＼ p))
+    lemma7 =  subst (λ k → filter P ∋ k ) (==→o≡ lemma5 ) lemma6
+    lemma8 : (q ∩ (L ＼ p)) ⊆ q
+    lemma8 = q∩q⊆q
 
-record Dense  (P : OD ) : Set (suc n) where
-   field
-       dense : OD
-       incl :  dense ⊆ P 
-       dense-f : OD → OD
-       dense-p :  { p : OD} → P ∋ p  → p ⊆ (dense-f p) 
+-----
+--
+--  if Filter contains L, prime filter is ultra
+--
 
--- H(ω,2) = Power ( Power ω ) = Def ( Def ω))
+filter-lemma2 :  {L : HOD} → (P : Filter L)  → filter P ∋ L → prime-filter P → ultra-filter P
+filter-lemma2 {L} P f∋L prime = record {
+         proper = prime-filter.proper prime
+       ; ultra = λ {p}  p⊆L → prime-filter.prime prime (lemma p  p⊆L)
+   } where
+        open _==_
+        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 → 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
 
-infinite = ZF.infinite OD→ZF
-
-module in-countable-ordinal {n : Level} where
+record Dense  (P : HOD ) : Set (suc n) where
+   field
+       dense : HOD
+       incl :  dense ⊆ P 
+       dense-f : HOD → HOD
+       dense-d :  { p : HOD} → P ∋ p  → dense ∋ dense-f p  
+       dense-p :  { p : HOD} → P ∋ p  →  p ⊆ (dense-f p) 
 
-   import ordinal
+--    the set of finite partial functions from ω to 2
+--
+--   ph2 : Nat → Set → 2
+--   ph2 : Nat → Maybe 2
+--
+-- Hω2 : Filter (Power (Power infinite))
 
-   -- open  ordinal.C-Ordinal-with-choice 
-   -- both Power and infinite is too ZF, it is better to use simpler one
-   Hω2 : Filter (Power (Power infinite))
-   Hω2 = {!!}
+record Ideal  ( L : HOD  ) : Set (suc n) where
+   field
+       ideal : HOD   
+       i⊆PL :  ideal ⊆ Power L 
+       ideal1 : { p q : HOD } →  q ⊆ L  → ideal ∋ p →  q ⊆ p  → ideal ∋ q
+       ideal2 : { p q : HOD } → ideal ∋ p →  ideal ∋ q  → ideal ∋ (p ∪ q)
 
+open Ideal
+
+proper-ideal : {L : HOD} → (P : Ideal L ) → {p : HOD} → Set n
+proper-ideal {L} P {p} = ideal P ∋ od∅
+
+prime-ideal : {L : HOD} → Ideal L → ∀ {p q : HOD } → Set n
+prime-ideal {L} P {p} {q} =  ideal P ∋ ( p ∩ q) → ( ideal P ∋ p ) ∨ ( ideal P ∋ q )
+
diff -r 9f926b2210bc -r ba3ebb9a16c6 ordinal.agda
--- a/ordinal.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -211,6 +211,7 @@
    ; o∅ = o∅
    ; osuc = osuc
    ; _o<_ = _o<_
+   ; next = next
    ; isOrdinal = record {
        Otrans = ordtrans
      ; OTri = trio<
@@ -218,14 +219,36 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
+     ; TransFinite1 = TransFinite2
+     ; not-limit = not-limit
+     ; next-limit = next-limit
    }
   } where
+     next : Ordinal {suc n} → Ordinal {suc n}
+     next (ordinal lv ord) = ordinal (Suc lv) (Φ (Suc lv))
+     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y)
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = lemma } where
+         lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
+         lemma x (case1 lt) = case1 lt
+     not-limit : (x : Ordinal) → Dec (¬ ((y : Ordinal) → ¬ (x ≡ osuc y)))
+     not-limit (ordinal lv (Φ lv)) = no (λ not → not (λ y () ))
+     not-limit (ordinal lv (OSuc lv ox)) = yes (λ not → not (ordinal lv ox) refl )
      ord1 : Set (suc n)
      ord1 = Ordinal {suc n}
-     TransFinite1 : { ψ : ord1  → Set (suc (suc n)) }
+     TransFinite1 : { ψ : ord1  → Set (suc n) }
           → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord1)  → ψ x
-     TransFinite1 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+     TransFinite1 {ψ} lt x = TransFinite {n} {suc n} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
+     TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
+          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord1)  → ψ x
+     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
         caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
             ψ (record { lv = lx ; ord = Φ lx })
         caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
@@ -233,3 +256,4 @@
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
 
+
diff -r 9f926b2210bc -r ba3ebb9a16c6 zf.agda
--- a/zf.agda	Sun Jun 07 20:35:14 2020 +0900
+++ b/zf.agda	Sun Jul 05 16:59:13 2020 +0900
@@ -49,7 +49,7 @@
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
      -- regularity without minimum
-     ε-induction : { ψ : ZFSet → Set (suc m)}
+     ε-induction : { ψ : ZFSet → Set m}
               → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
               → (x : ZFSet ) → ψ x
      -- infinity : ∃ A ( ∅ ∈ A ∧ ∀ x ∈ A ( x ∪ { x } ∈ A ) )