--- a/zf-in-agda.html	Wed Jul 15 08:42:30 2020 +0900
+++ b/zf-in-agda.html	Fri Jul 17 16:33:30 2020 +0900
@@ -940,7 +940,7 @@
 </pre>
 
 <hr/>
-<h2><a name="content039">Fixes on ZF to intuitionistic logic</a></h2>
+<h2><a name="content039">Fixing ZF axom to fit intuitionistic logic</a></h2>
 
 <p>
 We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
@@ -1205,6 +1205,27 @@
 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.
 <p>
+
+<hr/>
+<h2><a name="content048">HOD Ordrinal mapping</a></h2>
+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
+<p>
+
+<pre>
+    pair-xx&lt;xy : {x y : HOD} → od→ord (x , x) o&lt; osuc (od→ord (x , y) )
+    pair&lt;y : {x y : HOD } → y ∋ x  → od→ord (x , x) o&lt; osuc (od→ord y)
+
+</pre>
+Basicaly, we cannot know the concrete address of HOD other than empty set.
+<p>
+<img src="fig/address-of-HOD.svg">
+
+<p>
+
+<hr/>
+<h2><a name="content049">Possible restriction on HOD</a></h2>
 We need some restriction on the HOD-Ordinal mapping. Simple one is this.
 <p>
 
@@ -1229,18 +1250,8 @@
 <p>
 
 <hr/>
-<h2><a name="content048">increment pase of address of HOD</a></h2>
-The address of HOD may have obvious bound, but it is defined in a relative way.
-<p>
-
-<pre>
-    pair-xx&lt;xy : {x y : HOD} → od→ord (x , x) o&lt; osuc (od→ord (x , y) )
-    pair&lt;y : {x y : HOD } → y ∋ x  → od→ord (x , x) o&lt; osuc (od→ord y)
-
-</pre>
-Basicaly, we cannot know the concrete address of HOD other than empty set.
-<p>
-Assuming, previous assuption, we have 
+<h2><a name="content050">increment pase of address of HOD</a></h2>
+Assuming, hod-ord&lt; , we have 
 <p>
 
 <pre>
@@ -1249,8 +1260,13 @@
            lemmab0 : next (odmax (x , x)) ≡ next (od→ord x)
 
 </pre>
-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
 <p>
+
+<pre>
+    infinite-bound : ({x : HOD} → od→ord x o&lt; next (odmax x)) → {y : Ordinal} → infinite-d y → y o&lt; next o∅
+
+</pre>
 We also notice that if we have od→ord (x , x) ≡ osuc (od→ord x),  c&lt;→o&lt; can be drived from ⊆→o≤ . 
 <p>
 
@@ -1262,7 +1278,7 @@
 </pre>
 
 <hr/>
-<h2><a name="content049">Non constructive assumptions so far</a></h2>
+<h2><a name="content051">Non constructive assumptions so far</a></h2>
 
 <p>
 
@@ -1280,7 +1296,7 @@
 </pre>
 
 <hr/>
-<h2><a name="content050">Axiom which have negation form</a></h2>
+<h2><a name="content052">Axiom which have negation form</a></h2>
 
 <p>
 
@@ -1304,7 +1320,7 @@
 <p>
 
 <hr/>
-<h2><a name="content051">Union </a></h2>
+<h2><a name="content053">Union </a></h2>
 The original form of the Axiom of Union is
 <p>
 
@@ -1359,7 +1375,7 @@
 <p>
 
 <hr/>
-<h2><a name="content052">Axiom of replacement</a></h2>
+<h2><a name="content054">Axiom of replacement</a></h2>
 We can replace the elements of a set by a function and it becomes a set. From the book, 
 <p>
 
@@ -1410,7 +1426,7 @@
 <p>
 
 <hr/>
-<h2><a name="content053">Validity of Power Set Axiom</a></h2>
+<h2><a name="content055">Validity of Power Set Axiom</a></h2>
 The original Power Set Axiom is this.
 <p>
 
@@ -1503,7 +1519,7 @@
 </pre>
 
 <hr/>
-<h2><a name="content054">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
+<h2><a name="content056">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
 
 <p>
 Axiom of regularity requires non self intersectable elements (which is called minimum), if we
@@ -1550,7 +1566,7 @@
 <p>
 
 <hr/>
-<h2><a name="content055">Axiom of choice and Law of Excluded Middle</a></h2>
+<h2><a name="content057">Axiom of choice and Law of Excluded Middle</a></h2>
 In our model, since HOD has a mapping to Ordinals, it has evident order, which means well ordering theorem is valid,
 but it don't have correct form of the axiom yet. They say well ordering axiom is equivalent to the axiom of choice,
 but it requires law of the exclude middle.
@@ -1570,13 +1586,13 @@
 <p>
 
 <hr/>
-<h2><a name="content056">Relation-ship among ZF axiom</a></h2>
+<h2><a name="content058">Relation-ship among ZF axiom</a></h2>
 <img src="fig/axiom-dependency.svg">
 
 <p>
 
 <hr/>
-<h2><a name="content057">Non constructive assumption in our model</a></h2>
+<h2><a name="content059">Non constructive assumption in our model</a></h2>
 mapping between HOD and Ordinals
 <p>
 
@@ -1622,7 +1638,7 @@
 </pre>
 
 <hr/>
-<h2><a name="content058">So it this correct?</a></h2>
+<h2><a name="content060">So it this correct?</a></h2>
 
 <p>
 Our axiom are syntactically the same in the text book, but negations are slightly different.
@@ -1642,7 +1658,7 @@
 <p>
 
 <hr/>
-<h2><a name="content059">How to use Agda Set Theory</a></h2>
+<h2><a name="content061">How to use Agda Set Theory</a></h2>
 Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
 postulated or assuming law of excluded middle.
 <p>
@@ -1653,7 +1669,7 @@
 <p>
 
 <hr/>
-<h2><a name="content060">Topos and Set Theory</a></h2>
+<h2><a name="content062">Topos and Set Theory</a></h2>
 Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
 sub-object classifier. 
 <p>
@@ -1671,7 +1687,7 @@
 <p>
 
 <hr/>
-<h2><a name="content061">Cardinal number and Continuum hypothesis</a></h2>
+<h2><a name="content063">Cardinal number and Continuum hypothesis</a></h2>
 Axiom of choice is required to define cardinal number
 <p>
 definition of cardinal number is not yet done
@@ -1689,7 +1705,7 @@
 </pre>
 
 <hr/>
-<h2><a name="content062">Filter</a></h2>
+<h2><a name="content064">Filter</a></h2>
 
 <p>
 filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
@@ -1712,7 +1728,7 @@
 <p>
 
 <hr/>
-<h2><a name="content063">Programming Mathematics</a></h2>
+<h2><a name="content065">Programming Mathematics</a></h2>
 Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
 structure are
 <p>
@@ -1737,7 +1753,7 @@
 <p>
 
 <hr/>
-<h2><a name="content064">link</a></h2>
+<h2><a name="content066">link</a></h2>
 Summer school of foundation of mathematics (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/</a>
 <p>
 Foundation of axiomatic set theory (in Japanese)<br> <a href="https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf">https://www.sci.shizuoka.ac.jp/~math/yorioka/ss2019/sakai0.pdf
@@ -1796,7 +1812,7 @@
 <li><a href="#content036">  1 to 1 mapping between an HOD and an Ordinal</a>
 <li><a href="#content037">  Order preserving in the mapping of OD and Ordinal</a>
 <li><a href="#content038">  Various Sets</a>
-<li><a href="#content039">  Fixes on ZF to intuitionistic logic</a>
+<li><a href="#content039">  Fixing ZF axom to fit intuitionistic logic</a>
 <li><a href="#content040">  Pure logical axioms</a>
 <li><a href="#content041">  Axiom of Pair</a>
 <li><a href="#content042">  pair in OD</a>
@@ -1805,24 +1821,26 @@
 <li><a href="#content045">  Validity of Axiom of Extensionality</a>
 <li><a href="#content046">  Axiom of infinity</a>
 <li><a href="#content047">  ω in HOD</a>
-<li><a href="#content048">  increment pase of address of HOD</a>
-<li><a href="#content049">  Non constructive assumptions so far</a>
-<li><a href="#content050">  Axiom which have negation form</a>
-<li><a href="#content051">  Union </a>
-<li><a href="#content052">  Axiom of replacement</a>
-<li><a href="#content053">  Validity of Power Set Axiom</a>
-<li><a href="#content054">  Axiom of regularity, Axiom of choice, ε-induction</a>
-<li><a href="#content055">  Axiom of choice and Law of Excluded Middle</a>
-<li><a href="#content056">  Relation-ship among ZF axiom</a>
-<li><a href="#content057">  Non constructive assumption in our model</a>
-<li><a href="#content058">  So it this correct?</a>
-<li><a href="#content059">  How to use Agda Set Theory</a>
-<li><a href="#content060">  Topos and Set Theory</a>
-<li><a href="#content061">  Cardinal number and Continuum hypothesis</a>
-<li><a href="#content062">  Filter</a>
-<li><a href="#content063">  Programming Mathematics</a>
-<li><a href="#content064">  link</a>
+<li><a href="#content048">  HOD Ordrinal mapping</a>
+<li><a href="#content049">  Possible restriction on HOD</a>
+<li><a href="#content050">  increment pase of address of HOD</a>
+<li><a href="#content051">  Non constructive assumptions so far</a>
+<li><a href="#content052">  Axiom which have negation form</a>
+<li><a href="#content053">  Union </a>
+<li><a href="#content054">  Axiom of replacement</a>
+<li><a href="#content055">  Validity of Power Set Axiom</a>
+<li><a href="#content056">  Axiom of regularity, Axiom of choice, ε-induction</a>
+<li><a href="#content057">  Axiom of choice and Law of Excluded Middle</a>
+<li><a href="#content058">  Relation-ship among ZF axiom</a>
+<li><a href="#content059">  Non constructive assumption in our model</a>
+<li><a href="#content060">  So it this correct?</a>
+<li><a href="#content061">  How to use Agda Set Theory</a>
+<li><a href="#content062">  Topos and Set Theory</a>
+<li><a href="#content063">  Cardinal number and Continuum hypothesis</a>
+<li><a href="#content064">  Filter</a>
+<li><a href="#content065">  Programming Mathematics</a>
+<li><a href="#content066">  link</a>
 </ol>
 
-<hr/>  Shinji KONO /  Tue Jul 14 15:02:38 2020
+<hr/>  Shinji KONO /  Fri Jul 17 13:42:02 2020
 </body></html>