--- a/zf-in-agda.ind	Wed Jul 15 08:42:30 2020 +0900
+++ b/zf-in-agda.ind	Fri Jul 17 16:33:30 2020 +0900
@@ -671,7 +671,7 @@
     Agda Set / Type / it also has a level
 
 
---Fixes on ZF to intuitionistic logic
+--Fixing ZF axom to fit intuitionistic logic
 
 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
 ZF axioms in Agda.
@@ -854,6 +854,21 @@
 So what is the bound of ω? Analyzing the definition, it depends on the value of od→ord (x , x), which
 cannot know the aboslute value. This is because we don't have constructive definition of od→ord : HOD → Ordinal.
 
+--HOD Ordrinal mapping
+
+We have large freedom on HOD.  We reqest no minimality on odmax, so it may arbitrary larger.
+The address of HOD can be larger at least it have to be larger than the content's address.
+We only have a relative ordering such as
+
+    pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
+    pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
+
+Basicaly, we cannot know the concrete address of HOD other than empty set.
+
+<center><img src="fig/address-of-HOD.svg"></center>
+
+--Possible restriction on HOD
+
 We need some restriction on the HOD-Ordinal mapping. Simple one is this.
 
         ωmax : Ordinal
@@ -872,20 +887,15 @@
 
 --increment pase of address of HOD
 
-The address of HOD may have obvious bound, but it is defined in a relative way.
-
-    pair-xx<xy : {x y : HOD} → od→ord (x , x) o< osuc (od→ord (x , y) )
-    pair<y : {x y : HOD } → y ∋ x  → od→ord (x , x) o< osuc (od→ord y)
-
-Basicaly, we cannot know the concrete address of HOD other than empty set.
-
-Assuming, previous assuption, we have 
+Assuming, hod-ord< , we have 
 
     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)
 
-So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound.
+So the address of ( x , x) and Union (x , (x , x)) is restricted in the limit ordinal. This makes ω bound. We can prove
+
+    infinite-bound : ({x : HOD} → od→ord x o< next (odmax x)) → {y : Ordinal} → infinite-d y → y o< next o∅
 
 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x),  c<→o< can be drived from ⊆→o≤ .