# HG changeset patch # User Shinji KONO # Date 1594693048 -32400 # Node ID aa03b9c289c06dccca73b336770fe2868c6cf194 # Parent e4b7485b0b174ea4b08d967805f9c9ede1ac5551# Parent ba3ebb9a16c68a42615322daab3b1563bd9bcfe2 Limit Ordinal diff -r ba3ebb9a16c6 -r aa03b9c289c0 .hgtags --- 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 diff -r ba3ebb9a16c6 -r aa03b9c289c0 OD.agda --- 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 }; <-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) ; 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 ¬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 ; ¬a ¬b c | case1 eq = ⊥-elim (o<¬≡ (sym eq) oy ¬a ¬b c | case2 lt = ⊥-elim (o<> lt oy ¬a ¬b c = ⊥-elim (o<> (osucc c) oy ¬a ¬b c = ⊥-elim (¬nx 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 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 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 +there +

@@ -375,7 +377,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.

@@ -586,6 +589,7 @@

Classical story of ZF 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 @@

-

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. @@ -742,6 +746,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

@@ -765,30 +772,76 @@ 

-   record { def = λ x → true }
+   data One : Set n where
+      OneObj : One
+   record { def = λ x → One }
-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. +

+ +

+

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-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.

-

∋ in OD

-OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping +

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 

-      od→ord : OD  → Ordinal 
+     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 @@ -798,77 +851,47 @@ 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. -

-

Order preserving in the mapping of OD and Ordinal

-Ordinals have the order and OD has a natural order based on inclusion ( def / ∋ ). +

Order preserving in the mapping of OD and Ordinal

+Ordinals have the order and HOD has a natural order based on inclusion ( def / ∋ ). 

-     def y ( od→ord x )
+     def (od y) ( od→ord x )
-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. 

-  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
+  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)
-This is also said to be provable in classical Set Theory, but we simply assumes it. -

-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.

-

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.

@@ -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 @@ 

-    _,_ : 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.

@@ -1049,11 +1075,11 @@ 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 = ?
 
@@ -1064,16 +1090,16 @@
 

 
 
-   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
 
 

 
@@ -1081,39 +1107,38 @@
 
Validity of Axiom of Extensionality

 
 

-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
 

 
 
-  ==→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
+    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.
-

 
 

 
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 ψ 
 
 

 
@@ -1601,17 +1626,17 @@
 
  •   Classical story of ZF Set Theory
 
  •   Ordinals
 
  •   Axiom of Ordinals
-
  •   Concrete Ordinals
+
  •   Concrete Ordinals or Countable Ordinals
 
  •   Model of Ordinals
 
  •   Debugging axioms using Model
 
  •   Countable Ordinals can contains uncountable set?
 
  •   What is Set
 
  •   We don't ask the contents of Set. It can be anything.
 
  •   Ordinal Definable Set
-
  •   ∋ in OD
-
  •   1 to 1 mapping between an OD and an Ordinal
-
  •   Order preserving in the mapping of OD and Ordinal
-
  •   ISO
+
  •   OD is not ZF Set
+
  •    HOD : Hereditarily Ordinal Definable
+
  •   1 to 1 mapping between an HOD and an Ordinal
+
  •   Order preserving in the mapping of OD and Ordinal
 
  •   Various Sets
 
  •   Fixes on ZF to intuitionistic logic
 
  •   Pure logical axioms
@@ -1638,5 +1663,5 @@
 
  •   link
 
 
-
      Shinji KONO /  Sat May  9 16:41:10 2020
+
      Shinji KONO /  Tue Jul  7 15:44:35 2020
 
diff -r ba3ebb9a16c6 -r aa03b9c289c0 zf-in-agda.ind
--- 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 
+ 
+there
+
 
 --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
 
+
 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
+        
 
 --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.
 
 
    
 
---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 = ? ;