Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 354:aa03b9c289c0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Limit Ordinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Jul 2020 11:17:28 +0900
parents e4b7485b0b17 (diff) ba3ebb9a16c6 (current diff)
children 45fefbfd4871
files .hgtags
diffstat 8 files changed, 461 insertions(+), 174 deletions(-) [+]
line wrap: on
line diff
--- a/.hgtags	Sun Jul 05 16:59:13 2020 +0900
+++ b/.hgtags	Tue Jul 14 11:17:28 2020 +0900
@@ -23,3 +23,8 @@
 313140ae5e3d1793f8b2dc9055159658d63874e4 current
 313140ae5e3d1793f8b2dc9055159658d63874e4 current
 4fcac1eebc74af8ce383aeb9efd3230eecab5136 current
+12071f79f3cf40f788031e4f5ba83f6dcdbc91a0 current
+fcc65e37e72b007ee32a72d5d9b9c82db77927da release
+e0916a6329710d1a3ca7208ca7dfd3f0171299f1 curret
+12071f79f3cf40f788031e4f5ba83f6dcdbc91a0 current
+e277699923993f1bd91b34cb7c727725c96bc5f2 current
--- a/OD.agda	Sun Jul 05 16:59:13 2020 +0900
+++ b/OD.agda	Tue Jul 14 11:17:28 2020 +0900
@@ -96,22 +96,29 @@
   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)
+  ⊆→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 
+  ==→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
+-- possible order restriction
+hod-ord< :  {x : HOD } → Set n
+hod-ord< {x} =  od→ord x o< next (odmax x)
 
--- we have not this contradiction
--- bad-bad : ⊥
--- bad-bad = osuc-< <-osuc (c<→o< { record { od = record { def = λ x → One };  <odmax = {!!} } } OneObj)
+-- OD ⇔ Ordinal leads a contradiction, so we need bounded HOD
+¬OD-order : ( od→ord : OD  → Ordinal ) → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
+¬OD-order od→ord ord→od c<→o< = osuc-< <-osuc (c<→o< {Ords} OneObj )
+
+-- Open supreme upper bound leads a contradition, so we use domain restriction on sup
+¬open-sup : ( sup-o : (Ordinal →  Ordinal ) → Ordinal) → ((ψ : Ordinal →  Ordinal ) → (x : Ordinal) → ψ x  o<  sup-o ψ ) → ⊥
+¬open-sup sup-o sup-o< = o<> <-osuc (sup-o< next-ord (sup-o next-ord)) where
+   next-ord : Ordinal → Ordinal
+   next-ord x = osuc x
 
 -- Ordinal in OD ( and ZFSet ) Transitive Set
 Ord : ( a : Ordinal  ) → HOD 
@@ -125,14 +132,14 @@
 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)
+-- If we have reverse of c<→o<, everything becomes Ordinal
+o<→c<→HOD=Ord : ( o<→c< : {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 )
 
-
 _∋_ : ( a x : HOD  ) → Set n
 _∋_  a x  = odef a ( od→ord x )
 
@@ -208,12 +215,33 @@
 is-o∅ x | tri≈ ¬a b ¬c = yes b
 is-o∅ x | tri> ¬a ¬b c = no ¬b
 
-_,_ : HOD  → HOD  → HOD 
+-- the pair
+_,_ : 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  _ _
 
+pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
+pair-xx<xy {x} {y} = ⊆→o≤  lemma where
+   lemma : {z : Ordinal} → def (od (x , x)) z → def (od (x , y)) z
+   lemma {z} (case1 refl) = case1 refl
+   lemma {z} (case2 refl) = case1 refl
+
+--  another form of infinite
+-- pair-ord< :  {x : Ordinal } → Set n
+pair-ord< : {x : HOD } → ( {y : HOD } → od→ord y o< next (odmax y) ) → od→ord ( x , x ) o< next (od→ord x)
+pair-ord< {x} ho< = subst (λ k → od→ord (x , x) o< k ) lemmab0 lemmab1  where
+       lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
+       lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
+       lemmab1 : od→ord (x , x) o< next ( odmax (x , x))
+       lemmab1 = ho<
+
+pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
+pair<y {x} {y} y∋x = ⊆→o≤ lemma where
+   lemma : {z : Ordinal} → def (od (x , x)) z → def (od y) z
+   lemma (case1 refl) = y∋x
+   lemma (case2 refl) = y∋x
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
@@ -221,8 +249,6 @@
 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 → odef X (od→ord y )
-
 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)
@@ -235,15 +261,32 @@
 open _⊆_
 infixr  220 _⊆_
 
+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 )))
+
+-- if we have od→ord (x , x) ≡ osuc (od→ord x),  ⊆→o≤ → c<→o<
+⊆→o≤→c<→o< : ({x : HOD} → od→ord (x , x) ≡ osuc (od→ord x) )
+   →  ({y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o< osuc (od→ord z) )
+   →   {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o< od→ord y 
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x with trio< (od→ord x) (od→ord y)
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri< a ¬b ¬c = a
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ (peq {x}) (pair<y (subst (λ k → k ∋ x) (sym ( ==→o≡ {x} {y} (ord→== b))) y∋x )))
+⊆→o≤→c<→o< peq ⊆→o≤ {x} {y} y∋x | tri> ¬a ¬b c =
+  ⊥-elim ( o<> (⊆→o≤ {x , x} {y} y⊆x,x ) lemma1 ) where
+    lemma : {z : Ordinal} → (z ≡ od→ord x) ∨ (z ≡ od→ord x) → od→ord x ≡ z
+    lemma (case1 refl) = refl
+    lemma (case2 refl) = refl
+    y⊆x,x : {z : Ordinals.ord O} → def (od (x , x)) z → def (od y) z
+    y⊆x,x {z} lt = subst (λ k → def (od y) k ) (lemma lt) y∋x 
+    lemma1 : osuc (od→ord y) o< od→ord (x , x)
+    lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) 
+
 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))
@@ -260,6 +303,7 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
+-- level trick (what'a shame)
 ε-induction1 : { ψ : HOD  → Set (suc n)}
    → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
    → (x : HOD ) → ψ x
@@ -321,7 +365,7 @@
     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 
+    -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
     data infinite-d  : ( x : Ordinal  ) → Set n where
         iφ :  infinite-d o∅
@@ -329,10 +373,10 @@
                 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 nfinite-d y has a maximum.
+    -- We simply assumes infinite-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.
+    -- 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
@@ -341,6 +385,32 @@
     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))
+        lemma : {y : Ordinal} → infinite-d y → y o< next o∅
+        lemma {o∅} iφ = x<nx
+        lemma (isuc {y} x) = lemma2 where
+            lemma0 : y o< next o∅
+            lemma0 = lemma x
+            lemma8 : 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 : od→ord (ord→od y , ord→od y) o< next (od→ord (ord→od y))
+            lemma81 = nexto=n (subst (λ k →  od→ord (ord→od y , ord→od y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
+            lemma9 : 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 : od→ord (ord→od y , (ord→od y , ord→od y)) o< next (od→ord (ord→od y))
+            lemma71 = next< lemma81 lemma9
+            lemma1 : od→ord (u y) o< next (osuc (od→ord (ord→od y , (ord→od y , ord→od y))))
+            lemma1 = ho<
+            lemma2 : od→ord (u y) o< next o∅
+            lemma2 = next< lemma0 (next< (subst (λ k → od→ord (ord→od y , (ord→od y , ord→od y)) o< next k) diso lemma71 ) (nexto=n lemma1))
+        
+
     _=h=_ : (x y : HOD) → Set n
     x =h= y  = od x == od y
 
--- a/Ordinals.agda	Sun Jul 05 16:59:13 2020 +0900
+++ b/Ordinals.agda	Tue Jul 14 11:17:28 2020 +0900
@@ -20,8 +20,7 @@
      ¬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)  
-     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 )
+     not-limit-p :  ( x : ord  ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
@@ -29,6 +28,11 @@
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
 
+record IsNext {n : Level } (ord : Set n)  (o∅ : ord ) (osuc : ord → ord )  (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
+   field
+     x<nx :    { y : ord } → (y o< next y )
+     osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 
+     ¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)) 
 
 record Ordinals {n : Level} : Set (suc (suc n)) where
    field
@@ -38,6 +42,7 @@
      _o<_ : ord → ord → Set n
      next :  ord → ord
      isOrdinal : IsOrdinals ord o∅ osuc _o<_ next
+     isNext : IsNext ord o∅ osuc _o<_ next
 
 module inOrdinal  {n : Level} (O : Ordinals {n} ) where
 
@@ -61,7 +66,10 @@
         <-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)
+
+        x<nx = IsNext.x<nx (Ordinals.isNext O)
+        osuc<nx = IsNext.osuc<nx (Ordinals.isNext O) 
+        ¬nx<nx = IsNext.¬nx<nx (Ordinals.isNext O) 
 
         o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
         o<-dom  {x} _ = x
@@ -106,6 +114,12 @@
         osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy<ox)
         osucc {ox} {oy} oy<ox | tri> ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy<ox)
 
+        osucprev :  {ox oy : Ordinal } → osuc oy o< osuc ox  → oy o< ox  
+        osucprev {ox} {oy} oy<ox with trio< oy ox
+        osucprev {ox} {oy} oy<ox | tri< a ¬b ¬c = a
+        osucprev {ox} {oy} oy<ox | tri≈ ¬a b ¬c = ⊥-elim (o<¬≡ (cong (λ k → osuc k) b) oy<ox )
+        osucprev {ox} {oy} oy<ox | tri> ¬a ¬b c = ⊥-elim (o<> (osucc c) oy<ox )
+
         open _∧_
 
         osuc2 :  ( x y : Ordinal  ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
@@ -213,6 +227,35 @@
           → ¬ p
         FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
 
+        next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+        next< {x} {y} {z} x<nz y<nx with trio< y (next z)
+        next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
+        next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
+           (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
+        next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
+           (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
+
+        osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
+        osuc< {x} {y} refl = <-osuc 
+
+        nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y 
+        nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
+
+        nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)  
+        nexto≡ {x} with trio< (next x) (next (osuc x) ) 
+        --    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
+        nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
+           (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
+        nexto≡ {x} | tri≈ ¬a b ¬c = b
+        --    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
+        nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
+           (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
+
+        next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
+        next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
+            y<nx : y o< next x
+            y<nx = osuc< (sym eq)
+
         record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
           field
             os→ : (x : Ordinal) → x o< maxordinal → Ordinal
--- a/README.md	Sun Jul 05 16:59:13 2020 +0900
+++ b/README.md	Tue Jul 14 11:17:28 2020 +0900
@@ -1,1 +1,111 @@
-zf-in-agda.ind
\ No newline at end of file
+Constructing ZF Set Theory in Agda 
+============
+
+Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus
+
+## ZF in Agda
+
+```
+    zf.agda            axiom of ZF
+    zfc.agda           axiom of choice
+    Ordinals.agda      axiom of Ordinals
+    ordinal.agda       countable model of Ordinals
+    OD.agda            model of ZF based on Ordinal Definable Set with assumptions
+    ODC.agda           Law of exclude middle from axiom of choice assumptions
+    LEMC.agda          model of choice with assumption of the Law of exclude middle 
+    OPair.agda         ordered pair on OD
+
+    BAlgbra.agda       Boolean algebra on OD (not yet done)
+    filter.agda        Filter on OD (not yet done)
+    cardinal.agda      Caedinal number on OD (not yet done)
+
+    logic.agda         some basics on logic
+    nat.agda           some basics on Nat
+```
+
+## Ordinal Definable Set
+
+It is a predicate has an Ordinal argument.
+
+In Agda, OD is defined as follows.
+
+```
+    record OD : Set (suc n ) where
+      field
+        def : (x : Ordinal  ) → Set n
+```
+
+This is not a ZF Set, because it can contain entire Ordinals.
+
+## HOD : Hereditarily Ordinal Definable
+
+What we need is a bounded OD, the containment is limited by an ordinal.
+
+```
+    record HOD : Set (suc n) where
+      field
+        od : OD
+        odmax : Ordinal
+        <odmax : {y : Ordinal} → def od y → y o< odmax
+```
+
+In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
+
+```
+     HOD = { x | TC x ⊆ OD }
+```
+
+TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But 
+what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. 
+
+## 1 to 1 mapping between an HOD and an Ordinal
+
+HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
+
+```
+  od→ord : HOD  → Ordinal 
+  ord→od : Ordinal  → HOD  
+  oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
+  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
+```
+
+we can check an HOD is an element of the OD using def.
+
+A ∋ x can be define as follows.
+
+```
+    _∋_ : ( A x : HOD  ) → Set n
+    _∋_  A x  = def (od A) ( od→ord x )
+
+```
+In ψ : Ordinal → Set,  if A is a  record { def = λ x → ψ x } , then
+
+    A x = def A ( od→ord x ) = ψ (od→ord x)
+
+They say the existing of the mappings can be proved in Classical Set Theory, but we
+simply assumes these non constructively.
+
+## What have we done
+
+```
+    Axioms of Ordinals
+    An implementation of countable Ordinal
+    ZF Axioms
+    Model of ZF based on OD/HOD
+    LEM     axiom of choice from LEM
+    ODC     LEM from axiom of choice 
+    OPair   classical ordered pair example
+    filter  definition of filter and ideal
+    cardinal  unfinished Cardinal number
+    BAlgebra  boolean algebra of OD
+
+```
+
+
+
+
+
+
+
+
+
--- a/Todo	Sun Jul 05 16:59:13 2020 +0900
+++ b/Todo	Tue Jul 14 11:17:28 2020 +0900
@@ -2,7 +2,7 @@
 
     define cardinals 
     prove CH in OD→ZF
-    define Ultra filter
+    define Ultra filter  ... done
     define L M : ZF ZFSet = M is an OD
     define L N : ZF ZFSet = N = G M (G is a generic fitler on M )
     prove ¬ CH on L N
@@ -10,7 +10,7 @@
 
 Mon Jul  8 19:43:37 JST 2019
 
-    ordinal-definable.agda assumes all ZF Set are ordinals, that it too restrictive
+    ordinal-definable.agda assumes all ZF Set are ordinals, that it too restrictive  ... fixed
 
     remove ord-Ord  and prove with some assuption in HOD.agda
         union, power set, replace, inifinite
--- a/ordinal.agda	Sun Jul 05 16:59:13 2020 +0900
+++ b/ordinal.agda	Tue Jul 14 11:17:28 2020 +0900
@@ -226,10 +226,19 @@
   } 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
+     next-limit : {y : Ordinal} → (y o< next y) ∧ ((x : Ordinal) → x o< next y → osuc x o< next y) ∧
+        ( (x : Ordinal) → y o< x → x o< next y →  ¬ ((z : Ordinal) → ¬ (x ≡ osuc z)  ))
+     next-limit {y} = record { proj1 = case1 a<sa ; proj2 = record { proj1 = lemma ; proj2 = lemma2 } } where
          lemma :  (x : Ordinal) → x o< next y → osuc x o< next y
          lemma x (case1 lt) = case1 lt
+         lemma2 : (x : Ordinal) → y o< x → x o< next y → ¬ ((z : Ordinal) → ¬ x ≡ osuc z)
+         lemma2 (ordinal Zero (Φ 0)) (case2 ()) (case1 (s≤s z≤n)) not
+         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 Φ<) (case1 (s≤s z≤n)) not = not _ refl
+         lemma2 (ordinal Zero (OSuc 0 dx)) (case2 (s< x)) (case1 (s≤s z≤n)) not = not _ refl
+         lemma2 (ordinal (Suc lx) (OSuc (Suc lx) ox)) y<x (case1 (s≤s (s≤s lt))) not = not _ refl
+         lemma2 (ordinal (Suc lx) (Φ (Suc lx))) (case1 x) (case1 (s≤s (s≤s lt))) not = lemma3 x lt where
+             lemma3 : {n l : Nat} → (Suc (Suc n) ≤ Suc l) → l ≤ n → ⊥
+             lemma3   (s≤s sn≤l) (s≤s l≤n) = lemma3 sn≤l l≤n
      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 )
--- a/zf-in-agda.html	Sun Jul 05 16:59:13 2020 +0900
+++ b/zf-in-agda.html	Tue Jul 14 11:17:28 2020 +0900
@@ -98,7 +98,9 @@
 <p>
 I'm planning to do it in my old age, but I'm enough age now.
 <p>
-This is done during from May to September.
+if you familier with Agda, you can skip to <a href="#set-theory"> 
+there
+</a>
 <p>
 
 <hr/>
@@ -375,7 +377,8 @@
 <p>
 postulate can be constructive.
 <p>
-postulate can be inconsistent, which result everything has a proof.
+postulate can be inconsistent, which result everything has a proof. Actualy this assumption
+doesnot work for Ordinals, we discuss this later.
 <p>
 
 <hr/>
@@ -586,6 +589,7 @@
 <h2><a name="content023">Classical story of ZF Set Theory</a></h2>
 
 <p>
+<a name="set-theory">
 Assuming ZF, constructing  a model of ZF is a flow of classical Set Theory, which leads
 a relative consistency proof of the Set Theory.
 Ordinal number is used in the flow. 
@@ -647,7 +651,7 @@
 </pre>
 
 <hr/>
-<h2><a name="content026">Concrete Ordinals</a></h2>
+<h2><a name="content026">Concrete Ordinals or Countable Ordinals</a></h2>
 
 <p>
 We can define a list like structure with level, which is a kind of two dimensional infinite array.
@@ -742,6 +746,9 @@
 <p>
 But in our case, we have no ZF theory, so we are going to use Ordinals.
 <p>
+The idea is to use an ordinal as a pointer to a record which defines a Set.
+If the recored defines a series of Ordinals which is a pointer to the Set. This record  looks like a Set.
+<p>
 
 <hr/>
 <h2><a name="content032">Ordinal Definable Set</a></h2>
@@ -765,30 +772,76 @@
 <p>
 
 <pre>
-   record { def = λ x → true }
+   data One : Set n where
+      OneObj : One
+   record { def = λ x → One }
 
 </pre>
-means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
-but we don't care about it.
+means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set.
+You can say OD is a class in ZF Set Theory term.
+<p>
+
+<hr/>
+<h2><a name="content033">OD is not ZF Set</a></h2>
+If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like
+a Set.  The idea is to use an ordinal as a pointer to OD.
+Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like
+<p>
+
+<pre>
+   ¬OD-order : ( od→ord : OD  → Ordinal ) 
+      → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o&lt; od→ord y) → ⊥
+   ¬OD-order od→ord ord→od c&lt;→o&lt; = ?
+
+</pre>
+Actualy we can prove this contrdction, so we need some restrctions on OD.
+<p>
+This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself.
 <p>
 
 <hr/>
-<h2><a name="content033">∋ in OD</a></h2>
-OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
+<h2><a name="content034"> HOD : Hereditarily Ordinal Definable</a></h2>
+What we need is a bounded OD, the containment is limited by an ordinal.
+<p>
+
+<pre>
+    record HOD : Set (suc n) where
+      field
+        od : OD
+        odmax : Ordinal
+        &lt;odmax : {y : Ordinal} → def od y → y o&lt; odmax
+
+</pre>
+In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
 <p>
 
 <pre>
-      od→ord : OD  → Ordinal 
+     HOD = { x | TC x ⊆ OD }
 
 </pre>
-we may check an OD is an element of the OD using def.
+TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. 
+<p>
+
+<hr/>
+<h2><a name="content035">1 to 1 mapping between an HOD and an Ordinal</a></h2>
+HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
+<p>
+
+<pre>
+  od→ord : HOD  → Ordinal 
+  ord→od : Ordinal  → HOD  
+  oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
+  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
+
+</pre>
+we can check an HOD is an element of the OD using def.
 <p>
 A ∋ x can be define as follows.
 <p>
 
 <pre>
-    _∋_ : ( A x : OD  ) → Set n
-    _∋_  A x  = def A ( od→ord x )
+    _∋_ : ( A x : HOD  ) → Set n
+    _∋_  A x  = def (od A) ( od→ord x )
 
 </pre>
 In ψ : Ordinal → Set,  if A is a  record { def = λ x → ψ x } , then
@@ -798,77 +851,47 @@
     A x = def A ( od→ord x ) = ψ (od→ord x)
 
 </pre>
-
-<hr/>
-<h2><a name="content034">1 to 1 mapping between an OD and an Ordinal</a></h2>
-
-<p>
-
-<pre>
-  od→ord : OD  → Ordinal 
-  ord→od : Ordinal  → OD  
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-
-</pre>
 They say the existing of the mappings can be proved in Classical Set Theory, but we
 simply assumes these non constructively.
 <p>
-We use postulate, it may contains additional restrictions which are not clear now. It look like the mapping should be a subset of Ordinals, but we don't explicitly
-state it.
-<p>
 <img src="fig/ord-od-mapping.svg">
 
 <p>
 
 <hr/>
-<h2><a name="content035">Order preserving in the mapping of OD and Ordinal</a></h2>
-Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ).
+<h2><a name="content036">Order preserving in the mapping of OD and Ordinal</a></h2>
+Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ).
 <p>
 
 <pre>
-     def y ( od→ord x )
+     def (od y) ( od→ord x )
 
 </pre>
-An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements
+An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements
 have to be smaller than the corresponding ordinal of the containing OD.
+We also assumes subset is always smaller. This is necessary to make a limit of Power Set.
 <p>
 
 <pre>
-  c&lt;→o&lt;  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o&lt; od→ord y
+  c&lt;→o&lt;  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y
+  ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; osuc (od→ord z)
 
 </pre>
-This is also said to be provable in classical Set Theory, but we simply assumes it.
-<p>
-OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋relation. This means the reverse order preservation, 
+If wa assumes reverse order preservation, 
 <p>
 
 <pre>
   o&lt;→c&lt;  : {n : Level} {x y : Ordinal  } → x o&lt; y → def (ord→od y) x 
 
 </pre>
-is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in
-the model.
+∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
 <p>
 <img src="fig/ODandOrdinals.svg">
 
 <p>
 
 <hr/>
-<h2><a name="content036">ISO</a></h2>
-It also requires isomorphisms, 
-<p>
-
-<pre>
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-
-</pre>
-
-<hr/>
 <h2><a name="content037">Various Sets</a></h2>
-
-<p>
 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
 <p>
 
@@ -876,6 +899,7 @@
     Ordinal / things satisfies axiom of Ordinal / extension of natural number 
     V / hierarchical construction of Set from φ   
     L / hierarchical predicate definable construction of Set from φ   
+    HOD / Hereditarily Ordinal Definable
     OD / equational formula on Ordinals 
     Agda Set / Type / it also has a level
 
@@ -967,10 +991,12 @@
 <p>
 
 <pre>
-    _,_ : OD  → OD  → OD 
-    x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } 
+    _,_ : HOD  → HOD  → HOD 
+    x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = ? ; &lt;odmax = ? }
 
 </pre>
+It is easy to find out odmax from odmax of x and y.
+<p>
 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
 <p>
 
@@ -1049,11 +1075,11 @@
          eq← : ∀ { x : Ordinal  } → def b x → def a x
 
 </pre>
-Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B.
+Actually, (z : HOD) → (A ∋ z) ⇔ (B ∋ z) implies od A == od B.
 <p>
 
 <pre>
-    extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+    extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → od A == od B
     eq→ (extensionality0 {A} {B} eq ) {x} d = ?
     eq← (extensionality0 {A} {B} eq ) {x} d = ?
 
@@ -1064,16 +1090,16 @@
 <p>
 
 <pre>
-   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
+   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
 
 </pre>
 where
 <p>
 
 <pre>
-   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  → (def A (od y) → def (od B) y)  → def (od A) x → def (od B) x
+   odef-iso refl t = t
 
 </pre>
 
@@ -1081,39 +1107,38 @@
 <h2><a name="content044">Validity of Axiom of Extensionality</a></h2>
 
 <p>
-If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, so we assumes
+If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, so we assumes
 <p>
 
 <pre>
-  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+  ==→o≡ : { x y : HOD  } → (od x == od y) → x ≡ y
 
 </pre>
 Using this, we have
 <p>
 
 <pre>
-    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
+    proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
 
 </pre>
-This assumption means we may have an equivalence set on any predicates.
-<p>
 
 <hr/>
 <h2><a name="content045">Non constructive assumptions so far</a></h2>
-We have correspondence between OD and Ordinals and one directional order preserving.
-<p>
-We also have equality assumption.
+
 <p>
 
 <pre>
-  od→ord : OD  → Ordinal
-  ord→od : Ordinal  → OD
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  c&lt;→o&lt;  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o&lt; od→ord y
-  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+  od→ord : HOD  → Ordinal 
+  ord→od : Ordinal  → HOD  
+  c&lt;→o&lt;  :  {x y : HOD  }   → def (od y) ( od→ord x ) → od→ord x o&lt; od→ord y
+  ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → od→ord y o&lt; 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&lt; :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o&lt;  sup-o A ψ 
 
 </pre>
 
@@ -1601,17 +1626,17 @@
 <li><a href="#content023">  Classical story of ZF Set Theory</a>
 <li><a href="#content024">  Ordinals</a>
 <li><a href="#content025">  Axiom of Ordinals</a>
-<li><a href="#content026">  Concrete Ordinals</a>
+<li><a href="#content026">  Concrete Ordinals or Countable Ordinals</a>
 <li><a href="#content027">  Model of Ordinals</a>
 <li><a href="#content028">  Debugging axioms using Model</a>
 <li><a href="#content029">  Countable Ordinals can contains uncountable set?</a>
 <li><a href="#content030">  What is Set</a>
 <li><a href="#content031">  We don't ask the contents of Set. It can be anything.</a>
 <li><a href="#content032">  Ordinal Definable Set</a>
-<li><a href="#content033">  ∋ in OD</a>
-<li><a href="#content034">  1 to 1 mapping between an OD and an Ordinal</a>
-<li><a href="#content035">  Order preserving in the mapping of OD and Ordinal</a>
-<li><a href="#content036">  ISO</a>
+<li><a href="#content033">  OD is not ZF Set</a>
+<li><a href="#content034">   HOD : Hereditarily Ordinal Definable</a>
+<li><a href="#content035">  1 to 1 mapping between an HOD and an Ordinal</a>
+<li><a href="#content036">  Order preserving in the mapping of OD and Ordinal</a>
 <li><a href="#content037">  Various Sets</a>
 <li><a href="#content038">  Fixes on ZF to intuitionistic logic</a>
 <li><a href="#content039">  Pure logical axioms</a>
@@ -1638,5 +1663,5 @@
 <li><a href="#content060">  link</a>
 </ol>
 
-<hr/>  Shinji KONO /  Sat May  9 16:41:10 2020
+<hr/>  Shinji KONO /  Tue Jul  7 15:44:35 2020
 </body></html>
--- a/zf-in-agda.ind	Sun Jul 05 16:59:13 2020 +0900
+++ b/zf-in-agda.ind	Tue Jul 14 11:17:28 2020 +0900
@@ -54,7 +54,10 @@
 
 I'm planning to do it in my old age, but I'm enough age now.
 
-This is done during from May to September.
+if you familier with Agda, you can skip to 
+<a href="#set-theory"> 
+there
+</a>
 
 --Agda and Intuitionistic Logic 
 
@@ -262,7 +265,8 @@
 
 postulate can be constructive.
 
-postulate can be inconsistent, which result everything has a proof.
+postulate can be inconsistent, which result everything has a proof. Actualy this assumption
+doesnot work for Ordinals, we discuss this later.
 
 -- A ∨ B
 
@@ -403,6 +407,7 @@
  
 --Classical story of ZF Set Theory
 
+<a name="set-theory">
 Assuming ZF, constructing  a model of ZF is a flow of classical Set Theory, which leads
 a relative consistency proof of the Set Theory.
 Ordinal number is used in the flow. 
@@ -453,7 +458,7 @@
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
 
---Concrete Ordinals
+--Concrete Ordinals or Countable Ordinals
 
 We can define a list like structure with level, which is a kind of two dimensional infinite array.
 
@@ -525,6 +530,9 @@
 
 But in our case, we have no ZF theory, so we are going to use Ordinals.
 
+The idea is to use an ordinal as a pointer to a record which defines a Set.
+If the recored defines a series of Ordinals which is a pointer to the Set. 
+This record  looks like a Set.
 
 --Ordinal Definable Set
 
@@ -540,76 +548,93 @@
 
 Ordinals itself is not a set in a ZF Set theory but a class. In OD, 
 
-   record { def = λ x → true }
+   data One : Set n where
+      OneObj : One
 
-means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
-but we don't care about it.
+   record { def = λ x → One }
+
+means it accepets all Ordinals, i.e. this is Ordinals itself, so ODs are larger than ZF Set.
+You can say OD is a class in ZF Set Theory term.
 
 
---∋ in OD
+--OD is not ZF Set
+
+If we have 1 to 1 mapping between an OD and an Ordinal, OD contains several ODs and OD looks like
+a Set.  The idea is to use an ordinal as a pointer to OD.
+Unfortunately this scheme does not work well. As we saw OD includes all Ordinals, 
+which is a maximum of OD, but Ordinals has no maximum at all. So we have a contradction like
 
-OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
+   ¬OD-order : ( od→ord : OD  → Ordinal ) 
+      → ( ord→od : Ordinal  → OD ) → ( { x y : OD  }  → def y ( od→ord x ) → od→ord x o< od→ord y) → ⊥
+   ¬OD-order od→ord ord→od c<→o< = ?
+
+Actualy we can prove this contrdction, so we need some restrctions on OD.
+
+This is a kind of Russel paradox, that is if OD contains everything, what happens if it contains itself.
+
+-- HOD : Hereditarily Ordinal Definable
+
+What we need is a bounded OD, the containment is limited by an ordinal.
 
-      od→ord : OD  → Ordinal 
+    record HOD : Set (suc n) where
+      field
+        od : OD
+        odmax : Ordinal
+        <odmax : {y : Ordinal} → def od y → y o< odmax
+
+In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
+
+     HOD = { x | TC x ⊆ OD }
 
-we may check an OD is an element of the OD using def.
+TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But 
+what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. 
+
+--1 to 1 mapping between an HOD and an Ordinal
+
+HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
+
+  od→ord : HOD  → Ordinal 
+  ord→od : Ordinal  → HOD  
+  oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
+  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
+
+we can check an HOD is an element of the OD using def.
 
 A ∋ x can be define as follows.
 
-    _∋_ : ( A x : OD  ) → Set n
-    _∋_  A x  = def A ( od→ord x )
+    _∋_ : ( A x : HOD  ) → Set n
+    _∋_  A x  = def (od A) ( od→ord x )
 
 In ψ : Ordinal → Set,  if A is a  record { def = λ x → ψ x } , then
 
     A x = def A ( od→ord x ) = ψ (od→ord x)
 
---1 to 1 mapping between an OD and an Ordinal
-
-  od→ord : OD  → Ordinal 
-  ord→od : Ordinal  → OD  
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-
 They say the existing of the mappings can be proved in Classical Set Theory, but we
 simply assumes these non constructively.
 
-We use postulate, it may contains additional restrictions which are not clear now. 
-It look like the mapping should be a subset of Ordinals, but we don't explicitly
-state it.
-
 <center><img src="fig/ord-od-mapping.svg"></center>
 
 --Order preserving in the mapping of OD and Ordinal
 
-Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ).
+Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ).
 
-     def y ( od→ord x )
-
-An elements of OD should be defined before the OD, that is, an ordinal corresponding an elements
-have to be smaller than the corresponding ordinal of the containing OD.
+     def (od y) ( od→ord x )
 
-  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
+An elements of HOD should be defined before the HOD, that is, an ordinal corresponding an elements
+have to be smaller than the corresponding ordinal of the containing OD.
+We also assumes subset is always smaller. This is necessary to make a limit of Power Set.
 
-This is also said to be provable in classical Set Theory, but we simply assumes it.
+  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)
 
-OD has an order based on the corresponding ordinal, but it may not have corresponding def / ∋
-relation. This means the reverse order preservation, 
+If wa assumes reverse order preservation, 
 
   o<→c<  : {n : Level} {x y : Ordinal  } → x o< y → def (ord→od y) x 
 
-is not valid. If we assumes it, ∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in
-the model.
+∀ x ∋ ∅ becomes true, which manes all OD becomes Ordinals in the model.
 
 <center><img src="fig/ODandOrdinals.svg"></center>
 
---ISO
-
-It also requires isomorphisms, 
-
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-
-
 --Various Sets
 
 In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
@@ -617,6 +642,7 @@
     Ordinal / things satisfies axiom of Ordinal / extension of natural number 
     V / hierarchical construction of Set from φ   
     L / hierarchical predicate definable construction of Set from φ   
+    HOD / Hereditarily Ordinal Definable
     OD / equational formula on Ordinals 
     Agda Set / Type / it also has a level
 
@@ -682,8 +708,10 @@
 
 OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
 
-    _,_ : OD  → OD  → OD 
-    x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } 
+    _,_ : HOD  → HOD  → HOD 
+    x , y = record { od = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } ; odmax = ? ; <odmax = ? }
+
+It is easy to find out odmax from odmax of x and y.
 
 ≡ is an equality of λ terms, but please not that this is equality on Ordinals.
 
@@ -741,9 +769,9 @@
          eq→ : ∀ { x : Ordinal  } → def a x → def b x
          eq← : ∀ { x : Ordinal  } → def b x → def a x
 
-Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B.
+Actually, (z : HOD) → (A ∋ z) ⇔ (B ∋ z) implies od A == od B.
 
-    extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+    extensionality0 : {A B : HOD } → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → od A == od B
     eq→ (extensionality0 {A} {B} eq ) {x} d = ?
     eq← (extensionality0 {A} {B} eq ) {x} d = ?
 
@@ -751,41 +779,38 @@
 
 Actual proof is rather complicated.
 
-   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
+   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
 
 where
 
-   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  → (def A (od y) → def (od B) y)  → def (od A) x → def (od B) x
+   odef-iso refl t = t
 
 --Validity of Axiom of Extensionality
 
-If we can derive (w ∋ A) ⇔ (w ∋ B) from A == B, the axiom becomes valid, but it seems impossible, 
+If we can derive (w ∋ A) ⇔ (w ∋ B) from od A == od B, the axiom becomes valid, but it seems impossible, 
 so we assumes
 
-  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+  ==→o≡ : { x y : HOD  } → (od x == od y) → x ≡ y
 
 Using this, we have
 
-    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
-
-This assumption means we may have an equivalence set on any predicates.
+    proj2 (extensionality {A} {B} {w} eq ) d = subst (λ k → w ∋ k) (sym ( ==→o≡ (extensionality0 {A} {B} eq) )) d 
 
 --Non constructive assumptions so far
 
-We have correspondence between OD and Ordinals and one directional order preserving.
-
-We also have equality assumption.
-
-  od→ord : OD  → Ordinal
-  ord→od : Ordinal  → OD
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
-  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+  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 ψ 
 
 
 --Axiom which have negation form