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

changeset 361:4cbcf71b09c4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 17 Jul 2020 16:33:30 +0900
parents 2a8a51375e49
children 8a430df110eb
files OD.agda OPair.agda Ordinals.agda fig/ODandOrdinals.graffle fig/ODandOrdinals.svg fig/Sets.graffle fig/address-of-HOD.graffle fig/address-of-HOD.pdf fig/address-of-HOD.svg fig/axiom-type.graffle fig/axiom-type.svg fig/ord-od-mapping.graffle fig/ord-od-mapping.svg fig/set-theory.graffle fig/set-theory.svg zf-in-agda.html zf-in-agda.ind
diffstat 17 files changed, 363 insertions(+), 161 deletions(-) [+]
line wrap: on
line diff
--- a/OD.agda	Wed Jul 15 08:42:30 2020 +0900
+++ b/OD.agda	Fri Jul 17 16:33:30 2020 +0900
@@ -146,7 +146,7 @@
 _c<_ : ( x a : HOD  ) → Set n
 x c< a = a ∋ x 
 
-cseq : {n : Level} →  HOD  →  HOD 
+cseq :  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 ) 
@@ -154,7 +154,7 @@
 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
 
-otrans : {n : Level} {a x y : Ordinal  } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
+otrans : {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
 
 odef→o< :  {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X 
@@ -243,6 +243,10 @@
    lemma (case1 refl) = y∋x
    lemma (case2 refl) = y∋x
 
+-- another possible restriction. We reqest no minimality on odmax, so it may arbitrary larger.
+odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
+odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
+
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
--- a/OPair.agda	Wed Jul 15 08:42:30 2020 +0900
+++ b/OPair.agda	Fri Jul 17 16:33:30 2020 +0900
@@ -143,11 +143,29 @@
     checkAB : { p : Ordinal } → def ZFProduct p → Set n
     checkAB (pair x y) = odef A x ∧ odef B y
     pmax : Ordinal
-    pmax = omax (odmax A)  (odmax B)
-    <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)
-    <pmax {y} = TransFinite {λ y → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)} ind y where
-        ind : (x : Ordinal)
-            → ((y₁ : Ordinal) → y₁ o< x → def ZFProduct y₁ ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → y₁ o< (omax (odmax A) (odmax B)))
-            → def ZFProduct x ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → x o< (omax (HOD.odmax A) (HOD.odmax B))
-        ind = {!!}
+    pmax =  next (omax (od→ord A)  (od→ord B))
+    <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< next (omax (od→ord A)  (od→ord B))
+    <pmax {y} prod = {!!} where
+         prod-odmax : ( x y : HOD) → Ordinal
+         prod-odmax x y = omax (od→ord (x , x)) (od→ord (x , y))
+         lemma : {x y z : HOD } → ((x , x ) , (x , y )) ∋ z → od→ord z o< osuc (osuc (od→ord (x , y) ))
+         lemma {x} {y} {z} = {!!}
+         lemma1 : {x y  : HOD } → A ∋ x → B ∋ y → od→ord (x , y) o< omax (odmax A) (odmax B)
+         lemma1 {x} {y} A∋x  B∋y with trio< (odmax A) (odmax B)
+         lemma1 {x} {y} A∋x B∋y | tri< a ¬b ¬c = begin
+                 od→ord (x , y)
+              ≤⟨ {!!} ⟩
+                 odmax B
+              ∎ where open o≤-Reasoning O
+         lemma1 {x} {y} A∋x B∋y | tri≈ ¬a b ¬c = {!!}
+         lemma1 {x} {y} A∋x B∋y | tri> ¬a ¬b c = {!!}
 
+--            lemma2 : od→ord (x , y) o< osuc (omax (odmax A) (odmax B))
+--            lemma2 = begin
+--                 {!!}
+--              ≤⟨ {!!} ⟩
+--                 {!!}
+--              ∎ where open o≤-Reasoning O
+         a = π1 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
+         b = π2 (subst (λ k → def ZFProduct k) (sym diso) (proj1 prod))
+
--- a/Ordinals.agda	Wed Jul 15 08:42:30 2020 +0900
+++ b/Ordinals.agda	Fri Jul 17 16:33:30 2020 +0900
@@ -264,3 +264,30 @@
             os-iso← : {x : Ordinal} →  os→  (os← x) (os←limit x) ≡ x
             os-iso→ : {x : Ordinal} → (lt : x o< maxordinal ) →  os← (os→ x lt) ≡ x
 
+module o≤-Reasoning {n : Level} (O : Ordinals {n} )  where
+
+  open inOrdinal O
+
+  resp-o< : Ordinals._o<_ O Respects₂ _≡_
+  resp-o< =  resp₂ _o<_
+
+  trans1 : {i j k : Ordinal} → i o< j → j o< osuc  k → i o< k
+  trans1 {i} {j} {k} i<j j<ok with osuc-≡< j<ok
+  trans1 {i} {j} {k} i<j j<ok | case1 refl = i<j
+  trans1 {i} {j} {k} i<j j<ok | case2 j<k = ordtrans i<j j<k
+
+  trans2 : {i j k : Ordinal} → i o< osuc j → j o<  k → i o< k
+  trans2 {i} {j} {k} i<oj j<k with osuc-≡< i<oj
+  trans2 {i} {j} {k} i<oj j<k | case1 refl = j<k
+  trans2 {i} {j} {k} i<oj j<k | case2 i<j = ordtrans i<j j<k
+
+  open import Relation.Binary.Reasoning.Base.Triple {n} {_} {_} {_} {Ordinal } {_≡_} {_o≤_} {_o<_}
+    (Preorder.isPreorder OrdPreorder) 
+    ordtrans --<-trans
+     (resp₂ _o<_) --(resp₂ _<_)
+    (λ x → ordtrans x <-osuc ) --<⇒≤
+    trans1 --<-transˡ
+    trans2 --<-transʳ
+    public
+    hiding (_≈⟨_⟩_)
+
Binary file fig/ODandOrdinals.graffle has changed
--- a/fig/ODandOrdinals.svg	Wed Jul 15 08:42:30 2020 +0900
+++ b/fig/ODandOrdinals.svg	Fri Jul 17 16:33:30 2020 +0900
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
-<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="68 87 578 643" width="578" height="643">
+<svg xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns="http://www.w3.org/2000/svg" viewBox="68 87 586 582" width="586" height="582">
   <defs>
     <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-5 -3 6 6" markerWidth="6" markerHeight="6" color="black">
       <g>
@@ -17,13 +17,18 @@
         <path d="M 3.7333333 0 L 0 -1.4 L 0 1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
       </g>
     </marker>
+    <font-face font-family="Helvetica Neue" font-size="14" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
+      <font-face-src>
+        <font-face-name name="HelveticaNeue"/>
+      </font-face-src>
+    </font-face>
   </defs>
   <metadata> Produced by OmniGraffle 7.12.1 
-    <dc:date>2019-11-28 04:44:00 +0000</dc:date>
+    <dc:date>2020-07-16 05:25:36 +0000</dc:date>
   </metadata>
-  <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1">
+  <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none">
     <title>Canvas 1</title>
-    <rect fill="white" x="68" y="87" width="578" height="643"/>
+    <rect fill="white" x="68" y="87" width="586" height="582"/>
     <g id="Canvas_1: Layer 1">
       <title>Layer 1</title>
       <g id="Graphic_6">
@@ -46,10 +51,6 @@
         <ellipse cx="270.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" fill="white"/>
         <ellipse cx="270.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
-      <g id="Graphic_12">
-        <ellipse cx="293.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/>
-        <ellipse cx="293.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
-      </g>
       <g id="Graphic_13">
         <circle cx="154.5" cy="181.5" r="6.50001038636232" fill="black"/>
         <circle cx="154.5" cy="181.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
@@ -77,32 +78,26 @@
         <line x1="176.16929" y1="434.5874" x2="254.55825" y2="471.07884" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
       <g id="Line_21">
-        <line x1="173.96816" y1="195.3658" x2="277.63543" y2="269.20077" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+        <line x1="175.39975" y1="181.39705" x2="256" y2="181" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
       <g id="Line_22">
-        <line x1="178.3606" y1="273.87327" x2="277.5009" y2="279.5792" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+        <line x1="172.14058" y1="261.28998" x2="256" y2="208" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
       <g id="Line_23">
-        <line x1="178.05217" y1="300.43344" x2="277.50804" y2="283.2612" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+        <line x1="170.95411" y1="291.6123" x2="256" y2="225" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
       <g id="Graphic_24">
         <circle cx="150.21835" cy="525.5" r="6.50001038636231" fill="black"/>
         <circle cx="150.21835" cy="525.5" r="6.50001038636231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
       <g id="Line_25">
-        <line x1="162.28478" y1="504.8674" x2="278.23874" y2="306.5955" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+        <line x1="157.63988" y1="505.96074" x2="256" y2="247" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
       <g id="Graphic_26">
         <text transform="translate(119.245 633)" fill="black">
           <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan>
         </text>
       </g>
-      <g id="Graphic_27">
-        <text transform="translate(224.256 584)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan>
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan>
-        </text>
-      </g>
       <g id="Graphic_47">
         <path d="M 426 129 L 453.21835 251 L 480.4367 129 Z" fill="white"/>
         <path d="M 426 129 L 453.21835 251 L 480.4367 129 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
@@ -157,9 +152,8 @@
         </text>
       </g>
       <g id="Graphic_28">
-        <text transform="translate(527.256 584)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan>
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan>
+        <text transform="translate(549.454 584)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="27711167e-20" y="21">HOD</tspan>
         </text>
       </g>
       <g id="Line_48">
@@ -178,13 +172,34 @@
         </text>
       </g>
       <g id="Graphic_53">
-        <text transform="translate(377.204 92.608)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="7105427e-19" y="21">OD has a name in Ordinals</tspan>
+        <text transform="translate(369.262 92.608)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">HOD has a name in Ordinals</tspan>
+        </text>
+      </g>
+      <g id="Line_56">
+        <path d="M 256 133 L 256 272.21094 L 277.79297 272.21094 L 278 133" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_57">
+        <text transform="translate(255.47435 287.884)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan>
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan>
         </text>
       </g>
-      <g id="Graphic_54">
-        <text transform="translate(220 698)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">all arrows have to be acyclic</tspan>
+      <g id="Graphic_58">
+        <text transform="translate(221 584)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Hereditarily</tspan>
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="20.35" y="47.616">Ordinal</tspan>
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="9.361" y="74.231995">Definable</tspan>
+        </text>
+      </g>
+      <g id="Graphic_59">
+        <text transform="translate(297.46 219)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="7247536e-19" y="13">not bounded</tspan>
+        </text>
+      </g>
+      <g id="Graphic_60">
+        <text transform="translate(297.46 409.608)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">bounded</tspan>
         </text>
       </g>
     </g>
Binary file fig/Sets.graffle has changed
Binary file fig/address-of-HOD.graffle has changed
Binary file fig/address-of-HOD.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/address-of-HOD.svg	Fri Jul 17 16:33:30 2020 +0900
@@ -0,0 +1,113 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
+<svg xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns="http://www.w3.org/2000/svg" viewBox="253.785 161.5 248.185 537.116" width="248.185" height="537.116">
+  <defs>
+    <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -3 6 6" markerWidth="6" markerHeight="6" color="black">
+      <g>
+        <path d="M 3.7333333 0 L 0 -1.4 L 0 1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
+      </g>
+    </marker>
+    <font-face font-family="Helvetica Neue" font-size="22" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
+      <font-face-src>
+        <font-face-name name="HelveticaNeue"/>
+      </font-face-src>
+    </font-face>
+    <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-5 -3 6 6" markerWidth="6" markerHeight="6" color="black">
+      <g>
+        <path d="M -3.7333333 0 L 0 1.4 L 0 -1.4 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
+      </g>
+    </marker>
+    <font-face font-family="Helvetica Neue" font-size="14" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
+      <font-face-src>
+        <font-face-name name="HelveticaNeue"/>
+      </font-face-src>
+    </font-face>
+  </defs>
+  <metadata> Produced by OmniGraffle 7.12.1 
+    <dc:date>2020-07-16 09:18:05 +0000</dc:date>
+  </metadata>
+  <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none">
+    <title>Canvas 1</title>
+    <rect fill="white" x="253.785" y="161.5" width="248.185" height="537.116"/>
+    <g id="Canvas_1: Layer 1">
+      <title>Layer 1</title>
+      <g id="Graphic_17">
+        <path d="M 262.54 407 L 289.75835 529 L 316.9767 407 Z" fill="white"/>
+        <path d="M 262.54 407 L 289.75835 529 L 316.9767 407 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Line_22">
+        <path d="M 411.04 513.5 C 399.34904 489.1891 344.94662 458.1271 312.2266 439.7944" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_19">
+        <path d="M 262.54 163 L 289.75835 285 L 316.9767 163 Z" fill="white"/>
+        <path d="M 262.54 163 L 289.75835 285 L 316.9767 163 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_18">
+        <path d="M 262.54 285 L 289.75835 407 L 316.9767 285 Z" fill="white"/>
+        <path d="M 262.54 285 L 289.75835 407 L 316.9767 285 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_16">
+        <path d="M 262.54 529 L 289.75835 651 L 316.9767 529 Z" fill="white"/>
+        <path d="M 262.54 529 L 289.75835 651 L 316.9767 529 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_15">
+        <ellipse cx="410.04" cy="512.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/>
+        <ellipse cx="410.04" cy="512.5" rx="14.5000231695775" ry="82.5001318269065" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_13">
+        <circle cx="294.04" cy="215.5" r="6.50001038636234" fill="black"/>
+        <circle cx="294.04" cy="215.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_11">
+        <circle cx="294.04" cy="338.5" r="6.50001038636235" fill="black"/>
+        <circle cx="294.04" cy="338.5" r="6.50001038636235" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_10">
+        <circle cx="294.04" cy="429.5" r="6.50001038636236" fill="black"/>
+        <circle cx="294.04" cy="429.5" r="6.50001038636236" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_9">
+        <circle cx="294.04" cy="458.5" r="6.50001038636234" fill="black"/>
+        <circle cx="294.04" cy="458.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_8">
+        <circle cx="289.75835" cy="559.5" r="6.50001038636231" fill="black"/>
+        <circle cx="289.75835" cy="559.5" r="6.50001038636231" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_7">
+        <text transform="translate(258.785 667)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Ordinal</tspan>
+        </text>
+      </g>
+      <g id="Graphic_6">
+        <text transform="translate(367 608)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="37.07" y="21">HOD</tspan>
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="47.616">such as (x,y)</tspan>
+        </text>
+      </g>
+      <g id="Graphic_4">
+        <circle cx="289.75835" cy="183.5" r="6.50001038636233" fill="black"/>
+        <circle cx="289.75835" cy="183.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Line_21">
+        <path d="M 394.8927 484.52356 C 373.0247 446.2235 335.43026 385.45883 310.8905 355.36405" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Line_23">
+        <path d="M 432.15203 479.32975 C 465.39396 437.59087 508.5818 403.685 494 365 C 475.7518 316.58818 367.02 260.6628 300.54 222" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="12.0,12.0" stroke-width="3"/>
+      </g>
+      <g id="Line_24">
+        <path d="M 432.5173 470.00093 C 444.1753 446.3428 445.478 433.10376 433 400 C 415.3925 353.28783 364.2836 345.6657 300.99565 310.45614" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_12">
+        <circle cx="294.04" cy="306.5" r="6.50001038636234" fill="black"/>
+        <circle cx="294.04" cy="306.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_25">
+        <text transform="translate(373 207.608)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="15.309" y="13">The address of</tspan>
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="5755396e-19" y="29.392">HOD has a freedom</tspan>
+        </text>
+      </g>
+    </g>
+  </g>
+</svg>
Binary file fig/axiom-type.graffle has changed
--- a/fig/axiom-type.svg	Wed Jul 15 08:42:30 2020 +0900
+++ b/fig/axiom-type.svg	Fri Jul 17 16:33:30 2020 +0900
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
-<svg xmlns="http://www.w3.org/2000/svg" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="30 61 586 330" width="586" height="330">
+<svg xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns="http://www.w3.org/2000/svg" viewBox="30 61 567 330" width="567" height="330">
   <defs>
     <font-face font-family="Hiragino Sans" font-size="22" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300">
       <font-face-src>
@@ -19,11 +19,11 @@
     </font-face>
   </defs>
   <metadata> Produced by OmniGraffle 7.12.1 
-    <dc:date>2020-01-11 11:09:31 +0000</dc:date>
+    <dc:date>2020-07-16 05:11:34 +0000</dc:date>
   </metadata>
-  <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" fill="none" fill-opacity="1">
+  <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none">
     <title>Canvas 1</title>
-    <rect fill="white" x="30" y="61" width="586" height="330"/>
+    <rect fill="white" x="30" y="61" width="567" height="330"/>
     <g id="Canvas_1: Layer 1">
       <title>Layer 1</title>
       <g id="Graphic_2">
@@ -68,7 +68,7 @@
         </text>
       </g>
       <g id="Graphic_10">
-        <text transform="translate(454.8557 286.10003)" fill="black">
+        <text transform="translate(454.8557 303.86803)" fill="black">
           <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="9094947e-19" y="21">extensionarity</tspan>
         </text>
       </g>
@@ -93,12 +93,12 @@
         </text>
       </g>
       <g id="Graphic_20">
-        <text transform="translate(503.237 184.71603)" fill="black">
+        <text transform="translate(484.11375 184.71603)" fill="black">
           <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">ε-induction</tspan>
         </text>
       </g>
       <g id="Graphic_21">
-        <text transform="translate(478.057 322.71603)" fill="black">
+        <text transform="translate(470.1472 359.33202)" fill="black">
           <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">regularity</tspan>
         </text>
       </g>
@@ -118,7 +118,7 @@
         <line x1="174.272" y1="175.32412" x2="455.5455" y2="224.03823" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_29">
-        <line x1="174.272" y1="168.67903" x2="498.237" y2="193.25456" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="174.272" y1="168.90833" x2="479.11375" y2="193.05703" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_30">
         <line x1="198.114" y1="237.807" x2="310.19725" y2="228.40505" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
@@ -139,10 +139,15 @@
         <line x1="221.748" y1="344.74433" x2="334.057" y2="365.1827" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_36">
-        <line x1="221.748" y1="329.80394" x2="473.057" y2="334.73102" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="221.748" y1="338.57694" x2="465.1472" y2="366.55665" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_37">
-        <line x1="221.748" y1="321.31552" x2="449.8557" y2="304.74357" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="221.748" y1="325.4695" x2="449.8557" y2="319.1959" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Graphic_38">
+        <text transform="translate(430.7713 359.33202)" fill="black">
+          <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">=</tspan>
+        </text>
       </g>
     </g>
   </g>
Binary file fig/ord-od-mapping.graffle has changed
--- a/fig/ord-od-mapping.svg	Wed Jul 15 08:42:30 2020 +0900
+++ b/fig/ord-od-mapping.svg	Fri Jul 17 16:33:30 2020 +0900
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
-<svg version="1.1" xmlns="http://www.w3.org/2000/svg" xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="37 -5 449 664" width="449" height="664">
+<svg xmlns:xl="http://www.w3.org/1999/xlink" xmlns:dc="http://purl.org/dc/elements/1.1/" version="1.1" xmlns="http://www.w3.org/2000/svg" viewBox="37 -5 449 664" width="449" height="664">
   <defs>
     <font-face font-family="Helvetica Neue" font-size="22" panose-1="2 0 5 3 0 0 0 2 0 4" units-per-em="1000" underline-position="-100" underline-thickness="50" slope="0" x-height="517" cap-height="714" ascent="951.9958" descent="-212.99744" font-weight="400">
       <font-face-src>
@@ -12,6 +12,11 @@
         <font-face-name name="HelveticaNeue"/>
       </font-face-src>
     </font-face>
+    <font-face font-family="Hiragino Sans" font-size="14" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300">
+      <font-face-src>
+        <font-face-name name="HiraginoSans-W3"/>
+      </font-face-src>
+    </font-face>
     <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-1 -4 10 8" markerWidth="10" markerHeight="8" color="black">
       <g>
         <path d="M 8 0 L 0 -3 L 0 3 Z" fill="currentColor" stroke="currentColor" stroke-width="1"/>
@@ -19,9 +24,9 @@
     </marker>
   </defs>
   <metadata> Produced by OmniGraffle 7.12.1 
-    <dc:date>2019-11-28 05:45:48 +0000</dc:date>
+    <dc:date>2020-07-16 05:02:42 +0000</dc:date>
   </metadata>
-  <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1">
+  <g id="Canvas_1" fill-opacity="1" fill="none" stroke-opacity="1" stroke-dasharray="none" stroke="none">
     <title>Canvas 1</title>
     <rect fill="white" x="37" y="-5" width="449" height="664"/>
     <g id="Canvas_1: Layer 1">
@@ -52,19 +57,18 @@
         </text>
       </g>
       <g id="Graphic_5">
-        <text transform="translate(337 536)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="10.989" y="21">Ordinal</tspan>
-          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="5968559e-19" y="47.616">Definable</tspan>
+        <text transform="translate(289.326 536)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">Hereditarily Ordinal</tspan>
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="47.674" y="47.616">Definable</tspan>
         </text>
       </g>
       <g id="Graphic_20">
-        <text transform="translate(406.77 98.76035)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">max</tspan>
-          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x=".343" y="29.392">= all</tspan>
+        <text transform="translate(341.767 34)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="14210855e-21" y="13">max OD = all</tspan>
         </text>
       </g>
       <g id="Graphic_21">
-        <text transform="translate(440.722 509.608)" fill="black">
+        <text transform="translate(289.326 509.608)" fill="black">
           <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">empty</tspan>
         </text>
       </g>
@@ -74,43 +78,17 @@
           <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="29.392">max != Ordinal</tspan>
         </text>
       </g>
-      <g id="Line_23">
-        <line x1="255.471" y1="430.5664" x2="255.471" y2="534.5664" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
-      </g>
-      <g id="Line_24">
-        <line x1="236" y1="180" x2="236" y2="535" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
-      </g>
       <g id="Graphic_25">
-        <text transform="translate(99 509.608)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">empty</tspan>
+        <text transform="translate(211.755 509.608)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="14" font-weight="300" fill="black" x="0" y="12">φ</tspan>
         </text>
       </g>
       <g id="Line_27">
         <line x1="127" y1="535" x2="484.894" y2="535" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
-      <g id="Line_28">
-        <line x1="389" y1="140" x2="255.471" y2="430.5664" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
-      </g>
-      <g id="Line_31">
-        <line x1="389" y1="140" x2="236" y2="180.9972" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-dasharray="4.0,4.0" stroke-width="1"/>
-      </g>
-      <g id="Graphic_32">
-        <circle cx="242.5" cy="146.5" r="6.50001038636233" fill="black"/>
-        <circle cx="242.5" cy="146.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
-      </g>
-      <g id="Graphic_33">
-        <circle cx="255.971" cy="397.5" r="6.50001038636234" fill="black"/>
-        <circle cx="255.971" cy="397.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
-      </g>
       <g id="Graphic_34">
-        <circle cx="383.5" cy="115.15234" r="6.50001038636234" fill="black"/>
-        <circle cx="383.5" cy="115.15234" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
-      </g>
-      <g id="Line_35">
-        <line x1="250.3103" y1="144.76358" x2="375.6897" y2="116.88876" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
-      </g>
-      <g id="Line_36">
-        <line x1="380.20605" y1="122.44512" x2="259.26495" y2="390.20723" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <circle cx="333.5" cy="16.5" r="6.50001038636232" fill="black"/>
+        <circle cx="333.5" cy="16.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
       </g>
       <g id="Line_40">
         <line x1="372.3718" y1="630.664" x2="246.9" y2="630.664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
@@ -137,37 +115,37 @@
         </text>
       </g>
       <g id="Line_46">
-        <line x1="399" y1="370" x2="414.93724" y2="273.84283" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="330.222" y1="370" x2="346.15924" y2="273.84283" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Graphic_45">
-        <text transform="translate(433.218 318.13017)" fill="black">
-          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">defined</tspan>
-          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="15.687" y="29.392">by</tspan>
+        <text transform="translate(352.771 318.13017)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="2.072" y="13">defined by </tspan>
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="29.392">or included</tspan>
         </text>
       </g>
       <g id="Line_47">
-        <line x1="399" y1="450" x2="399" y2="375.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="330.222" y1="450" x2="330.222" y2="375.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_48">
-        <line x1="416.556" y1="474.9336" x2="416.556" y2="400.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="347.778" y1="474.9336" x2="347.778" y2="400.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_49">
-        <line x1="407.778" y1="507.9336" x2="407.778" y2="433.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="339" y1="507.9336" x2="339" y2="433.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_50">
-        <line x1="391.54" y1="209.0664" x2="400.23237" y2="153.77986" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="322.762" y1="209.0664" x2="331.45437" y2="153.77986" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_51">
-        <line x1="412" y1="243.9336" x2="412" y2="169.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="343.222" y1="243.9336" x2="343.222" y2="169.9" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_52">
-        <line x1="391.54" y1="307" x2="391.54" y2="218.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="322.762" y1="307" x2="322.762" y2="218.9664" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_53">
-        <line x1="416.556" y1="264.07607" x2="431.52065" y2="216.44483" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="347.778" y1="264.07607" x2="362.74265" y2="216.44483" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Line_54">
-        <line x1="399" y1="366.0664" x2="392.7805" y2="316.82197" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        <line x1="330.222" y1="366.0664" x2="324.0025" y2="316.82197" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
       </g>
       <g id="Graphic_55">
         <text transform="translate(107 610.272)" fill="black">
@@ -179,6 +157,20 @@
           <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="17053026e-20" y="13">Partial order</tspan>
         </text>
       </g>
+      <g id="Graphic_57">
+        <text transform="translate(253.792 509.608)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="7274181e-19" y="13">=</tspan>
+        </text>
+      </g>
+      <g id="Line_58">
+        <line x1="343.222" y1="151.9668" x2="342.36764" y2="93.89893" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Graphic_59">
+        <text transform="translate(357.433 89)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="1.946" y="13">HOD has </tspan>
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="7.133" y="29.392">no max</tspan>
+        </text>
+      </g>
     </g>
   </g>
 </svg>
Binary file fig/set-theory.graffle has changed
--- a/fig/set-theory.svg	Wed Jul 15 08:42:30 2020 +0900
+++ b/fig/set-theory.svg	Fri Jul 17 16:33:30 2020 +0900
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <!DOCTYPE svg PUBLIC "-//W3C//DTD SVG 1.1//EN" "http://www.w3.org/Graphics/SVG/1.1/DTD/svg11.dtd">
-<svg xmlns="http://www.w3.org/2000/svg" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:xl="http://www.w3.org/1999/xlink" version="1.1" viewBox="38.294 90.49994 434.607 310.5001" width="434.607" height="310.5001">
+<svg version="1.1" xmlns:xl="http://www.w3.org/1999/xlink" xmlns="http://www.w3.org/2000/svg" xmlns:dc="http://purl.org/dc/elements/1.1/" viewBox="38.294 90.49994 434.607 310.5001" width="434.607" height="310.5001">
   <defs>
     <font-face font-family="Hiragino Sans" font-size="22" panose-1="2 11 3 0 0 0 0 0 0 0" units-per-em="1000" underline-position="-75" underline-thickness="50" slope="0" x-height="545" cap-height="766" ascent="880.0018" descent="-120.00024" font-weight="300">
       <font-face-src>
@@ -14,9 +14,9 @@
     </font-face>
   </defs>
   <metadata> Produced by OmniGraffle 7.12.1 
-    <dc:date>2020-01-11 11:07:37 +0000</dc:date>
+    <dc:date>2020-07-16 04:53:15 +0000</dc:date>
   </metadata>
-  <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" fill="none" fill-opacity="1">
+  <g id="Canvas_1" stroke-dasharray="none" stroke="none" stroke-opacity="1" fill="none" fill-opacity="1">
     <title>Canvas 1</title>
     <rect fill="white" x="38.294" y="90.49994" width="434.607" height="310.5001"/>
     <g id="Canvas_1: Layer 1">
@@ -79,8 +79,8 @@
         </text>
       </g>
       <g id="Graphic_16">
-        <text transform="translate(292.522 348.5)" fill="black">
-          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Model on OD</tspan>
+        <text transform="translate(283.964 348.5)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="5684342e-20" y="19">Model on HOD</tspan>
         </text>
       </g>
       <g id="Graphic_19">
--- 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>
--- 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≤ .