changeset 273:9ccf8514c323

add documents
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 11 Jan 2020 20:11:51 +0900
parents 985a1af11bce
children 29a85a427ed2
files fig/ODandOrdinals.graffle fig/ODandOrdinals.svg fig/Sets.graffle fig/Sets.svg fig/axiom-dependency.graffle fig/axiom-dependency.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 14 files changed, 3517 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
Binary file fig/ODandOrdinals.graffle has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/ODandOrdinals.svg	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,192 @@
+<?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">
+  <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>
+        <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="-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>
+  </defs>
+  <metadata> Produced by OmniGraffle 7.12.1 
+    <dc:date>2019-11-28 04:44:00 +0000</dc:date>
+  </metadata>
+  <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1">
+    <title>Canvas 1</title>
+    <rect fill="white" x="68" y="87" width="578" height="643"/>
+    <g id="Canvas_1: Layer 1">
+      <title>Layer 1</title>
+      <g id="Graphic_6">
+        <path d="M 123 129 L 150.21835 251 L 177.4367 129 Z" fill="white"/>
+        <path d="M 123 129 L 150.21835 251 L 177.4367 129 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_7">
+        <path d="M 123 251 L 150.21835 373 L 177.4367 251 Z" fill="white"/>
+        <path d="M 123 251 L 150.21835 373 L 177.4367 251 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_8">
+        <path d="M 123 373 L 150.21835 495 L 177.4367 373 Z" fill="white"/>
+        <path d="M 123 373 L 150.21835 495 L 177.4367 373 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_9">
+        <path d="M 123 495 L 150.21835 617 L 177.4367 495 Z" fill="white"/>
+        <path d="M 123 495 L 150.21835 617 L 177.4367 495 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_10">
+        <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"/>
+      </g>
+      <g id="Graphic_14">
+        <circle cx="154.5" cy="272.5" r="6.50001038636234" fill="black"/>
+        <circle cx="154.5" cy="272.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_15">
+        <circle cx="154.5" cy="304.5" r="6.50001038636234" fill="black"/>
+        <circle cx="154.5" cy="304.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_16">
+        <circle cx="154.5" cy="395.5" r="6.50001038636233" fill="black"/>
+        <circle cx="154.5" cy="395.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_18">
+        <circle cx="154.5" cy="424.5" r="6.50001038636234" fill="black"/>
+        <circle cx="154.5" cy="424.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Line_19">
+        <line x1="173.9379" y1="409.40815" x2="254.63666" y2="467.1495" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Line_20">
+        <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"/>
+      </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"/>
+      </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"/>
+      </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"/>
+      </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"/>
+      </g>
+      <g id="Graphic_46">
+        <path d="M 426 251 L 453.21835 373 L 480.4367 251 Z" fill="white"/>
+        <path d="M 426 251 L 453.21835 373 L 480.4367 251 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_45">
+        <path d="M 426 373 L 453.21835 495 L 480.4367 373 Z" fill="white"/>
+        <path d="M 426 373 L 453.21835 495 L 480.4367 373 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_44">
+        <path d="M 426 495 L 453.21835 617 L 480.4367 495 Z" fill="white"/>
+        <path d="M 426 495 L 453.21835 617 L 480.4367 495 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_43">
+        <ellipse cx="573.5" cy="478.5" rx="14.5000231695775" ry="82.5001318269064" fill="white"/>
+        <ellipse cx="573.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_42">
+        <ellipse cx="596.5" cy="280.5" rx="14.5000231695775" ry="82.5001318269065" fill="white"/>
+        <ellipse cx="596.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_41">
+        <circle cx="457.5" cy="181.5" r="6.50001038636232" fill="black"/>
+        <circle cx="457.5" cy="181.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_40">
+        <circle cx="457.5" cy="272.5" r="6.50001038636234" fill="black"/>
+        <circle cx="457.5" cy="272.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_39">
+        <circle cx="457.5" cy="304.5" r="6.50001038636234" fill="black"/>
+        <circle cx="457.5" cy="304.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_38">
+        <circle cx="457.5" cy="395.5" r="6.50001038636232" fill="black"/>
+        <circle cx="457.5" cy="395.5" r="6.50001038636232" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_37">
+        <circle cx="457.5" cy="424.5" r="6.50001038636234" fill="black"/>
+        <circle cx="457.5" cy="424.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_31">
+        <circle cx="453.21835" cy="525.5" r="6.50001038636233" fill="black"/>
+        <circle cx="453.21835" cy="525.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_29">
+        <text transform="translate(422.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_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>
+      </g>
+      <g id="Line_48">
+        <path d="M 604.7609 469.93216 C 612.0671 467.7524 618.9377 465.6045 624.34375 463.84375 C 637.5514 459.5421 639.2045 425.7619 633.77734 414.5703 C 628.35015 403.3787 602 397 574 385 C 546 373 545 374 507 358 C 469 342 416.78393 326.70416 398 311 C 379.21607 295.29584 381.79114 286.83255 383 279 C 384.20886 271.16745 393.904 266.09114 404 266 C 410.17797 265.94423 421.8459 265.70735 434.2442 267.17386" marker-end="url(#FilledArrow_Marker_2)" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_49">
+        <circle cx="453.21835" cy="149.5" r="6.50001038636234" fill="black"/>
+        <circle cx="453.21835" cy="149.5" r="6.50001038636234" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Line_50">
+        <path d="M 623.554 268.5201 C 625.4985 267.62867 627.6082 266.779 630 266 C 643.2077 261.69835 643.4272 246.1916 638 235 C 632.5728 223.8084 607 201 559 210 C 511 219 518.4367 243 480.4367 227 C 442.4367 211 413.62724 203.75242 394.8433 188.04826 C 376.0594 172.3441 378.63445 163.88081 379.8433 156.04826 C 381.05217 148.21571 390.7473 143.1394 400.8433 143.04826 C 408.3246 142.98073 423.85655 142.6476 438.987 145.39538" marker-end="url(#FilledArrow_Marker_2)" marker-start="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_52">
+        <text transform="translate(73.912 92.608)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="18474111e-20" y="21">OD contains Ordinals</tspan>
+        </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>
+      </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>
+        </text>
+      </g>
+    </g>
+  </g>
+</svg>
Binary file fig/Sets.graffle has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/Sets.svg	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,84 @@
+<?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="26 93 572 303" width="572" height="303">
+  <defs>
+    <font-face font-family="Hiragino Sans" font-size="18" 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>
+    <font-face font-family="Helvetica Neue" font-size="18" 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-27 13:34:32 +0000</dc:date>
+  </metadata>
+  <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1">
+    <title>Canvas 1</title>
+    <rect fill="white" x="26" y="93" width="572" height="303"/>
+    <g id="Canvas_1: Layer 1">
+      <title>Layer 1</title>
+      <g id="Graphic_2">
+        <text transform="translate(133 98.00003)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">様々な集合</tspan>
+        </text>
+      </g>
+      <g id="Graphic_4">
+        <text transform="translate(108 137.00001)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">順序数の公理を満たすもの。自然数の延長</tspan>
+        </text>
+      </g>
+      <g id="Graphic_5">
+        <text transform="translate(108 176)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">一つ一つ増やす。無限回繰り返して、それを全部。</tspan>
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">また一つ一つ増やすを繰り返して得られるもの</tspan>
+        </text>
+      </g>
+      <g id="Graphic_6">
+        <text transform="translate(108 233.696)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">述語で定義されるものを集めるのを繰り返して作られるもの</tspan>
+        </text>
+      </g>
+      <g id="Graphic_7">
+        <text transform="translate(108 281.99994)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">順序数上の方程式を満たす順序数の集合</tspan>
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">階層化されていない</tspan>
+        </text>
+      </g>
+      <g id="Graphic_8">
+        <text transform="translate(31.59 137.00001)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">Ordinal</tspan>
+        </text>
+      </g>
+      <g id="Graphic_9">
+        <text transform="translate(54.936 176)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">V</tspan>
+        </text>
+      </g>
+      <g id="Graphic_10">
+        <text transform="translate(53.23 281.99994)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="0" y="17">OD</tspan>
+        </text>
+      </g>
+      <g id="Graphic_11">
+        <text transform="translate(55.816 233.696)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="8144596e-19" y="17">L</tspan>
+        </text>
+      </g>
+      <g id="Graphic_12">
+        <text transform="translate(51.174 336)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="18" font-weight="400" fill="black" x="2.502" y="17">Set </tspan>
+        </text>
+      </g>
+      <g id="Graphic_13">
+        <text transform="translate(108 336)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="16">型。集まりではなく、値の種類を区別する記号。’</tspan>
+          <tspan font-family="Hiragino Sans" font-size="18" font-weight="300" fill="black" x="0" y="43.00002">自身が値になると、一つLevelの高い型を持つ</tspan>
+        </text>
+      </g>
+    </g>
+  </g>
+</svg>
Binary file fig/axiom-dependency.graffle has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/axiom-dependency.svg	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,87 @@
+<?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="28 101 424 224" width="424" height="224">
+  <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>
+        <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"/>
+      </g>
+    </marker>
+    <marker orient="auto" overflow="visible" markerUnits="strokeWidth" id="FilledArrow_Marker_2" stroke-linejoin="miter" stroke-miterlimit="10" viewBox="-9 -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"/>
+      </g>
+    </marker>
+  </defs>
+  <metadata> Produced by OmniGraffle 7.12.1 
+    <dc:date>2020-01-11 11:10:39 +0000</dc:date>
+  </metadata>
+  <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" fill="none" fill-opacity="1">
+    <title>Canvas 1</title>
+    <rect fill="white" x="28" y="101" width="424" height="224"/>
+    <g id="Canvas_1: Layer 1">
+      <title>Layer 1</title>
+      <g id="Graphic_18">
+        <rect x="30" y="103" width="420" height="166" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_2">
+        <text transform="translate(334.578 126)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="48316906e-20" y="19">Choice</tspan>
+        </text>
+      </g>
+      <g id="Graphic_3">
+        <text transform="translate(347.91 223.00002)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="14566126e-20" y="19">LEM</tspan>
+        </text>
+      </g>
+      <g id="Graphic_4">
+        <text transform="translate(133.323 286)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8952838e-19" y="19">Well ordering outside</tspan>
+        </text>
+      </g>
+      <g id="Graphic_7">
+        <text transform="translate(83 180)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">ε-induction</tspan>
+        </text>
+      </g>
+      <g id="Graphic_8">
+        <text transform="translate(43.556 126)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Strong Regularity</tspan>
+        </text>
+      </g>
+      <g id="Line_9">
+        <line x1="240" y1="142.50001" x2="319.678" y2="142.50001" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_10">
+        <line x1="372" y1="164.00002" x2="372" y2="208.10002" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Graphic_11">
+        <text transform="translate(110.66 223.00002)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Well ordering inside</tspan>
+        </text>
+      </g>
+      <g id="Line_12">
+        <line x1="218.438" y1="179.55565" x2="319.95423" y2="155.05904" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Group_16">
+        <g id="Line_14">
+          <line x1="240" y1="156" x2="272.71875" y2="188.27344" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        </g>
+        <g id="Line_15">
+          <line x1="274" y1="156" x2="240" y2="188.23828" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+        </g>
+      </g>
+      <g id="Line_17">
+        <line x1="372" y1="218.00002" x2="372" y2="173.90002" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_19">
+        <line x1="329.6113" y1="169.28897" x2="260.9037" y2="212.71107" marker-end="url(#FilledArrow_Marker)" marker-start="url(#FilledArrow_Marker_2)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+    </g>
+  </g>
+</svg>
Binary file fig/axiom-type.graffle has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/axiom-type.svg	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,149 @@
+<?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">
+  <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>
+        <font-face-name name="HiraginoSans-W3"/>
+      </font-face-src>
+    </font-face>
+    <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>
+    <font-face font-family="Helvetica" font-size="22" units-per-em="1000" underline-position="-75.68359" underline-thickness="49.316406" slope="0" x-height="522.9492" cap-height="717.28516" ascent="770.0195" descent="-229.98047" font-weight="400">
+      <font-face-src>
+        <font-face-name name="Helvetica"/>
+      </font-face-src>
+    </font-face>
+  </defs>
+  <metadata> Produced by OmniGraffle 7.12.1 
+    <dc:date>2020-01-11 11:09:31 +0000</dc:date>
+  </metadata>
+  <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" fill="none" fill-opacity="1">
+    <title>Canvas 1</title>
+    <rect fill="white" x="30" y="61" width="586" height="330"/>
+    <g id="Canvas_1: Layer 1">
+      <title>Layer 1</title>
+      <g id="Graphic_2">
+        <text transform="translate(184.9378 66)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="19895197e-20" y="19">Axioms of Set theory in Agda</tspan>
+        </text>
+      </g>
+      <g id="Graphic_3">
+        <text transform="translate(42.728 147)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8526513e-19" y="19">Pure logical</tspan>
+        </text>
+      </g>
+      <g id="Graphic_4">
+        <text transform="translate(35 228.358)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="6963319e-19" y="19">Negation form</tspan>
+        </text>
+      </g>
+      <g id="Graphic_5">
+        <text transform="translate(42.728 295)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="22737368e-20" y="19">Non construtive</tspan>
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="18.205" y="52.00002">assumptions</tspan>
+        </text>
+      </g>
+      <g id="Graphic_6">
+        <text transform="translate(418.057 127.71603)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">pair</tspan>
+        </text>
+      </g>
+      <g id="Graphic_7">
+        <text transform="translate(315.19725 212.40404)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="0" y="21">union</tspan>
+        </text>
+      </g>
+      <g id="Graphic_8">
+        <text transform="translate(315.2768 109.00002)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="24868996e-20" y="21">empty</tspan>
+        </text>
+      </g>
+      <g id="Graphic_9">
+        <text transform="translate(299.057 255.71603)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="7993606e-19" y="21">power</tspan>
+        </text>
+      </g>
+      <g id="Graphic_10">
+        <text transform="translate(454.8557 286.10003)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="9094947e-19" y="21">extensionarity</tspan>
+        </text>
+      </g>
+      <g id="Graphic_11">
+        <text transform="translate(460.5455 217.10003)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="45474735e-20" y="21">infinity</tspan>
+        </text>
+      </g>
+      <g id="Graphic_16">
+        <text transform="translate(488.237 148.71603)" fill="black">
+          <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">selection</tspan>
+        </text>
+      </g>
+      <g id="Graphic_18">
+        <text transform="translate(454.8557 249.02004)" fill="black">
+          <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">replacement</tspan>
+        </text>
+      </g>
+      <g id="Graphic_19">
+        <text transform="translate(339.057 358.71603)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="22" font-weight="400" fill="black" x="7531753e-19" y="21">choice</tspan>
+        </text>
+      </g>
+      <g id="Graphic_20">
+        <text transform="translate(503.237 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">
+          <tspan font-family="Helvetica" font-size="22" font-weight="400" fill="black" x="0" y="21">regularity</tspan>
+        </text>
+      </g>
+      <g id="Line_23">
+        <line x1="174.272" y1="158.8584" x2="413.057" y2="142.6241" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_24">
+        <line x1="174.272" y1="163.21387" x2="483.237" y2="161.91894" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_25">
+        <line x1="174.272" y1="181.47427" x2="310.19725" y2="217.25989" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_26">
+        <line x1="174.272" y1="151.78494" x2="310.2768" y2="128.44731" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_27">
+        <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"/>
+      </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"/>
+      </g>
+      <g id="Line_31">
+        <line x1="198.114" y1="254.2734" x2="294.057" y2="265.02016" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_32">
+        <line x1="198.114" y1="248.45253" x2="449.8557" y2="259.2177" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_33">
+        <line x1="221.748" y1="312.25824" x2="449.8557" y2="273.2318" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_34">
+        <line x1="221.748" y1="300.8768" x2="294.057" y2="279.56114" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Line_35">
+        <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"/>
+      </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"/>
+      </g>
+    </g>
+  </g>
+</svg>
Binary file fig/ord-od-mapping.graffle has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/ord-od-mapping.svg	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,184 @@
+<?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">
+  <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>
+        <font-face-name name="HelveticaNeue"/>
+      </font-face-src>
+    </font-face>
+    <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>
+    <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"/>
+      </g>
+    </marker>
+  </defs>
+  <metadata> Produced by OmniGraffle 7.12.1 
+    <dc:date>2019-11-28 05:45:48 +0000</dc:date>
+  </metadata>
+  <g id="Canvas_1" stroke-dasharray="none" stroke="none" fill="none" stroke-opacity="1" fill-opacity="1">
+    <title>Canvas 1</title>
+    <rect fill="white" x="37" y="-5" width="449" height="664"/>
+    <g id="Canvas_1: Layer 1">
+      <title>Layer 1</title>
+      <g id="Graphic_18">
+        <path d="M 159 49 L 186.21835 171 L 213.4367 49 Z" fill="white"/>
+        <path d="M 159 49 L 186.21835 171 L 213.4367 49 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_17">
+        <path d="M 159 171 L 186.21835 293 L 213.4367 171 Z" fill="white"/>
+        <path d="M 159 171 L 186.21835 293 L 213.4367 171 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_16">
+        <path d="M 159 293 L 186.21835 415 L 213.4367 293 Z" fill="white"/>
+        <path d="M 159 293 L 186.21835 415 L 213.4367 293 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_15">
+        <path d="M 159 415 L 186.21835 537 L 213.4367 415 Z" fill="white"/>
+        <path d="M 159 415 L 186.21835 537 L 213.4367 415 Z" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_12">
+        <circle cx="186.21835" cy="16.5" r="6.50001038636233" fill="black"/>
+        <circle cx="186.21835" cy="16.5" r="6.50001038636233" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_6">
+        <text transform="translate(155.245 553)" 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_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>
+      </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>
+      </g>
+      <g id="Graphic_21">
+        <text transform="translate(440.722 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>
+      <g id="Graphic_22">
+        <text transform="translate(42 .10800171)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="23.261" y="13">Ordinal</tspan>
+          <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>
+      </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"/>
+      </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"/>
+      </g>
+      <g id="Line_39">
+        <line x1="188" y1="622.218" x2="365.575" y2="622.218" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Graphic_38">
+        <text transform="translate(253.792 599.232)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">non-order preserving</tspan>
+        </text>
+      </g>
+      <g id="Graphic_37">
+        <text transform="translate(260.471 636.664)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">order preserving</tspan>
+        </text>
+      </g>
+      <g id="Line_41">
+        <line x1="107" y1="356" x2="107" y2="274.47422" marker-end="url(#FilledArrow_Marker)" stroke="black" stroke-linecap="round" stroke-linejoin="round" stroke-width="1"/>
+      </g>
+      <g id="Graphic_44">
+        <text transform="translate(45.888 318.13017)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="4973799e-19" y="13">larger</tspan>
+        </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"/>
+      </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>
+      </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"/>
+      </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"/>
+      </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"/>
+      </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"/>
+      </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"/>
+      </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"/>
+      </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"/>
+      </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"/>
+      </g>
+      <g id="Graphic_55">
+        <text transform="translate(107 610.272)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="0" y="13">Total order</tspan>
+        </text>
+      </g>
+      <g id="Graphic_56">
+        <text transform="translate(395 614.522)" fill="black">
+          <tspan font-family="Helvetica Neue" font-size="14" font-weight="400" fill="black" x="17053026e-20" y="13">Partial order</tspan>
+        </text>
+      </g>
+    </g>
+  </g>
+</svg>
Binary file fig/set-theory.graffle has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/fig/set-theory.svg	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,93 @@
+<?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">
+  <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>
+        <font-face-name name="HiraginoSans-W3"/>
+      </font-face-src>
+    </font-face>
+    <font-face font-family="Hiragino Sans" font-size="16" 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>
+  </defs>
+  <metadata> Produced by OmniGraffle 7.12.1 
+    <dc:date>2020-01-11 11:07:37 +0000</dc:date>
+  </metadata>
+  <g id="Canvas_1" stroke-opacity="1" stroke-dasharray="none" stroke="none" 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">
+      <title>Layer 1</title>
+      <g id="Graphic_21">
+        <rect x="55" y="323.5" width="172" height="76.000045" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_22">
+        <rect x="278" y="323.5" width="172" height="76.000045" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_20">
+        <rect x="55" y="260.5" width="172" height="59.5" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_18">
+        <rect x="278" y="197.5" width="172" height="122.5" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_17">
+        <rect x="55" y="197.5" width="172" height="59.5" stroke="gray" stroke-linecap="round" stroke-linejoin="round" stroke-width="3"/>
+      </g>
+      <g id="Graphic_2">
+        <text transform="translate(43.294 95.49994)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="58264504e-20" y="19">primitive set theory</tspan>
+        </text>
+      </g>
+      <g id="Graphic_4">
+        <text transform="translate(68.66 138.49996)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="22.858" y="19">First order</tspan>
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="5968559e-19" y="52.00002">predicate logic</tspan>
+        </text>
+      </g>
+      <g id="Graphic_5">
+        <text transform="translate(78.849 279.75004)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8597567e-19" y="19">Ordinals</tspan>
+        </text>
+      </g>
+      <g id="Graphic_6">
+        <text transform="translate(76.954 340.5001)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="19895197e-20" y="19">Model on ZF</tspan>
+        </text>
+      </g>
+      <g id="Graphic_10">
+        <text transform="translate(270.099 171.49999)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">Higher order logic</tspan>
+        </text>
+      </g>
+      <g id="Graphic_13">
+        <text transform="translate(292.522 210.75)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="8597567e-19" y="19">Ordinals</tspan>
+        </text>
+      </g>
+      <g id="Graphic_14">
+        <text transform="translate(292.522 242.25)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">ZF axioms</tspan>
+        </text>
+      </g>
+      <g id="Graphic_15">
+        <text transform="translate(285.475 272.25003)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="16" font-weight="300" fill="black" x="3.573997" y="14">Non constructive</tspan>
+          <tspan font-family="Hiragino Sans" font-size="16" font-weight="300" fill="black" x="21.437997" y="38.000016">assumptions</tspan>
+        </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>
+      </g>
+      <g id="Graphic_19">
+        <text transform="translate(77.021 210.99999)" fill="black">
+          <tspan font-family="Hiragino Sans" font-size="22" font-weight="300" fill="black" x="0" y="19">ZF axioms</tspan>
+        </text>
+      </g>
+    </g>
+  </g>
+</svg>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/zf-in-agda.html	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,1619 @@
+<html>
+<META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=UTF-8">
+<head>
+<STYLE type="text/css">
+.main { width:100%; }
+.side { top:0px; width:0%; position:fixed; left:80%; display:none}
+</STYLE>
+<script type="text/javascript">
+function showElement(layer){
+    var myLayer = document.getElementById(layer);
+    var main = document.getElementById('mmm');
+    if(myLayer.style.display=="none"){
+        myLayer.style.width="20%";
+        main.style.width="80%";
+        myLayer.style.display="block";
+        myLayer.backgroundPosition="top";
+    } else { 
+        myLayer.style.width="0%";
+        main.style.width="100%";
+        myLayer.style.display="none";
+    }
+}
+</script>
+<title>Constructing ZF Set Theory in Agda </title>
+</head>
+<body>
+<div class="main" id="mmm">
+<h1>Constructing ZF Set Theory in Agda </h1>
+<a href="#" right="0px" onclick="javascript:showElement('menu')">
+<span>Menu</span>
+</a>
+<a href="#" left="0px" onclick="javascript:showElement('menu')">
+<span>Menu</span>
+</a>
+
+<p>
+
+<author> Shinji KONO</author>
+
+<hr/>
+<h2><a name="content000">Programming Mathematics</a></h2>
+Programming is processing data structure with λ terms.
+<p>
+We are going to handle Mathematics in intuitionistic logic with λ terms.
+<p>
+Mathematics is a functional programming which values are proofs.
+<p>
+Programming ZF Set Theory in Agda
+<p>
+
+<hr/>
+<h2><a name="content001">Target</a></h2>
+
+<pre>
+   Describe ZF axioms in Agda
+   Construction a Model of ZF Set Theory in Agda
+   Show necessary assumptions for the model
+   Show validities of ZF axioms on the model
+
+</pre>
+This shows consistency of Set Theory (with some assumptions),
+without circulating ZF Theory assumption.
+<p>
+<a href="https://github.com/shinji-kono/zf-in-agda">
+ZF in Agda https://github.com/shinji-kono/zf-in-agda
+</a>
+<p>
+
+<hr/>
+<h2><a name="content002">Why Set Theory</a></h2>
+If we can formulate Set theory, it suppose to work on any mathematical theory.
+<p>
+Set Theory is a difficult point for beginners especially axiom of choice.
+<p>
+It has some amount of difficulty and self circulating discussion.
+<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.
+<p>
+
+<hr/>
+<h2><a name="content003">Agda and Intuitionistic Logic </a></h2>
+Curry Howard Isomorphism
+<p>
+
+<pre>
+    Proposition : Proof ⇔ Type : Value
+
+</pre>
+which means
+<p>
+  constructing a typed lambda calculus which corresponds a logic
+<p>
+Typed lambda calculus which allows complex type as a value of a variable (System FC)
+<p>
+  First class Type / Dependent Type
+<p>
+Agda is a such a programming language which has similar syntax of Haskell
+<p>
+Coq is specialized in proof assistance such as command and tactics .
+<p>
+
+<hr/>
+<h2><a name="content004">Introduction of Agda </a></h2>
+A length of a list of type A.
+<p>
+
+<pre>
+    length : {A : Set } → List A → Nat
+    length [] = zero
+    length (_ ∷ t)  = suc ( length t )
+
+</pre>
+Simple functional programming language. Type declaration is mandatory.
+A colon means type, an equal means value. Indentation based.
+<p>
+Set is a base type (which may have a level ).
+<p>
+{} means implicit variable which can be omitted if Agda infers its value.
+<p>
+
+<hr/>
+<h2><a name="content005">data ( Sum type )</a></h2>
+A data type which as exclusive multiple constructors. A similar one as
+union in C or case class in Scala.
+<p>
+It has a similar syntax as Haskell but it has a slight difference.
+<p>
+
+<pre>
+   data List (A : Set ) : Set where
+        [] : List A
+        _∷_ : A → List A → List A
+
+</pre>
+_∷_ means infix operator. If use explicit _, it can be used in a normal function
+syntax.
+<p>
+Natural number can be defined as a usual way.
+<p>
+
+<pre>
+   data Nat : Set where
+        zero : Nat
+        suc  : Nat → Nat
+
+</pre>
+
+<hr/>
+<h2><a name="content006"> A → B means "A implies B"</a></h2>
+
+<p>
+In Agda, a type can be a value of a variable, which is usually called dependent type.
+Type has a name Set in Agda.
+<p>
+
+<pre>
+    ex3 : {A B : Set} → Set 
+    ex3 {A}{B}  =  A → B
+
+</pre>
+ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B.
+<p>
+
+<pre>
+    A type is a formula, the value is the proof
+
+</pre>
+A value of A → B can be interpreted as an inference from the formula A to the formula B, which
+can be a function from a proof of A to a proof of B.
+<p>
+
+<hr/>
+<h2><a name="content007">introduction と elimination</a></h2>
+For a logical operator, there are two types of inference, an introduction and an elimination.
+<p>
+
+<pre>
+  intro creating symbol  / constructor / introduction
+  elim  using symbolic / accessors / elimination
+
+</pre>
+In Natural deduction, this can be written in proof schema.
+<p>
+
+<pre>
+       A                   
+       :
+       B                    A       A → B
+   ------------- →intro   ------------------ →elim
+      A → B                     B
+
+</pre>
+In Agda, this is a pair of type and value as follows. Introduction of → uses λ.
+<p>
+
+<pre>
+    →intro : {A B : Set } → A →  B → ( A → B )
+    →intro _ b = λ x → b
+    →elim : {A B : Set } → A → ( A → B ) → B
+    →elim a f = f a
+
+</pre>
+Important
+<p>
+
+<pre>
+    {A B : Set } → A →  B → ( A → B )
+
+</pre>
+is
+<p>
+
+<pre>
+    {A B : Set } → ( A →  ( B → ( A → B ) ))
+
+</pre>
+This makes currying of function easy.
+<p>
+
+<hr/>
+<h2><a name="content008"> To prove A → B </a></h2>
+Make a left type as an argument. (intros in Coq)
+<p>
+
+<pre>
+    ex5 : {A B C : Set } → A → B → C  → ?
+    ex5 a b c = ?
+
+</pre>
+? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole.
+<p>
+We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red),
+insufficient proof or instance (Yellow), Non-termination, the proof is completed.
+<p>
+
+<hr/>
+<h2><a name="content009"> A ∧ B</a></h2>
+Well known conjunction's introduction and elimination is as follow.
+<p>
+
+<pre>
+     A    B                 A ∧ B           A ∧ B 
+   -------------         ----------- proj1   ---------- proj2
+      A ∧ B                   A               B
+
+</pre>
+We can introduce a corresponding structure in our functional programming language.
+<p>
+
+<hr/>
+<h2><a name="content010"> record</a></h2>
+
+<pre>
+   record _∧_ A B : Set
+     field
+         proj1 : A
+         proj2 : B
+
+</pre>
+_∧_ means infix operator.  _∧_ A B can be written as  A ∧  B (Haskell uses (∧) )
+<p>
+This a type which constructed from type A and type B. You may think this as an object
+or struct.
+<p>
+
+<pre>
+   record { proj1 = x ; proj2 = y }    
+
+</pre>
+is a constructor of _∧_.
+<p>
+
+<pre>
+    ex3 : {A B : Set} → A → B → ( A ∧ B )
+    ex3 a b = record { proj1 = a ; proj2 = b }
+    ex1 : {A B : Set} → ( A ∧ B ) → A
+    ex1 a∧b = proj1 a∧b
+
+</pre>
+a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols
+except parenthesis or colons. A symbol requires space separation such as a type defining colon.
+<p>
+Defining record can be recursively, but we don't use the recursion here.
+<p>
+
+<hr/>
+<h2><a name="content011"> Mathematical structure</a></h2>
+We have types of elements and the relationship in a mathematical structure.
+<p>
+
+<pre>
+  logical relation has no ordering
+  there is a natural ordering in arguments and a value in a function
+
+</pre>
+So we have typical definition style of mathematical structure with records.
+<p>
+
+<pre>
+  record IsOrdinals {n : Level} (ord : Set n)  
+    (_o&lt;_ : ord → ord → Set n) : Set (suc (suc n)) where
+   field
+     Otrans :  {x y z : ord }  → x o&lt; y → y o&lt; z → x o&lt; z
+  record Ordinals {n : Level} : Set (suc (suc n)) where
+       field 
+         ord : Set n
+         _o&lt;_ : ord → ord → Set n
+         isOrdinal : IsOrdinals ord _o&lt;_
+
+</pre>
+In IsOrdinals, axioms are written in flat way. In Ordinal, we may have
+inputs and outputs are put in the field including IsOrdinal.
+<p>
+Fields of Ordinal is existential objects in the mathematical structure.
+<p>
+
+<hr/>
+<h2><a name="content012"> A Model and a theory</a></h2>
+Agda record is a type, so we can write it in the argument, but is it really exists?
+<p>
+If we have a value of the record, it simply exists, that is, we need to create all the existence
+in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
+<p>
+
+<pre>
+   type of record = theory
+   value of record = model
+
+</pre>
+We call the value of the record as a model. If mathematical structure has a
+model, it exists. Pretty Obvious.
+<p>
+
+<hr/>
+<h2><a name="content013"> postulate と module</a></h2>
+Agda proofs are separated by modules, which are large records.
+<p>
+postulates are assumptions. We can assume a type without proofs.
+<p>
+
+<pre>
+    postulate      
+      sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal 
+      sup-o&lt; :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o&lt;  sup-o ψ 
+
+</pre>
+sup-o is an example of upper bound of a function and sup-o&lt; assumes it actually satisfies all the value is less than upper bound.
+<p>
+Writing some type in a module argument is the same as postulating a type, but
+postulate can be written the middle of a proof.
+<p>
+postulate can be constructive.
+<p>
+postulate can be inconsistent, which result everything has a proof.
+<p>
+
+<hr/>
+<h2><a name="content014"> A ∨ B</a></h2>
+
+<pre>
+    data _∨_ (A B : Set) : Set where
+      case1 : A → A ∨ B
+      case2 : B → A ∨ B
+
+</pre>
+As Haskell, case1/case2 are  patterns.
+<p>
+
+<pre>
+    ex3 : {A B : Set} → ( A ∨ A ) → A 
+    ex3 = ?
+
+</pre>
+In a case statement, Agda command C-C C-C generates possible cases in the head.
+<p>
+
+<pre>
+    ex3 : {A B : Set} → ( A ∨ A ) → A 
+    ex3 (case1 x) = ?
+    ex3 (case2 x) = ?
+
+</pre>
+Proof schema of ∨ is omit due to the complexity.
+<p>
+
+<hr/>
+<h2><a name="content015"> Negation</a></h2>
+
+<pre>
+       ⊥
+    ------------- ⊥-elim
+       A
+
+</pre>
+Anything can be derived from bottom, in this case a Set A. There is no introduction rule
+in ⊥, which can be implemented as data which has no constructor.
+<p>
+
+<pre>
+    data ⊥ : Set where
+
+</pre>
+⊥-elim can be proved like this.
+<p>
+
+<pre>
+    ⊥-elim : {A : Set } -&gt; ⊥ -&gt; A
+    ⊥-elim ()
+
+</pre>
+() means no match argument nor value.
+<p>
+A negation can be defined using ⊥ like this.
+<p>
+
+<pre>
+    ¬_ : Set → Set
+    ¬ A = A → ⊥
+
+</pre>
+
+<hr/>
+<h2><a name="content016">Equality </a></h2>
+
+<p>
+All the value in Agda are terms. If we have the same normalized form, two terms are equal.
+If we have variables in the terms, we will perform an unification. unifiable terms are equal.
+We don't go further on the unification.
+<p>
+
+<pre>
+     { x : A }                 x ≡ y    f x y
+   --------------- ≡-intro   --------------------- ≡-elim
+      x ≡ x                         f x x
+
+</pre>
+equality _≡_  can be defined as a data.
+<p>
+
+<pre>
+    data _≡_ {A : Set } : A → A → Set where
+       refl :  {x : A} → x ≡ x
+
+</pre>
+The elimination of equality is a substitution in a term.
+<p>
+
+<pre>
+    subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
+    subst {A} {x} {y} f refl fx = fx
+    ex5 :   {A : Set} {x y z : A } →  x ≡ y → y ≡ z → x ≡ z
+    ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
+
+</pre>
+
+<hr/>
+<h2><a name="content017">Equivalence relation</a></h2>
+
+<p>
+
+<pre>
+    refl' : {A : Set} {x : A } → x ≡ x
+    refl'  = ?
+    sym : {A : Set} {x y : A } → x ≡ y → y ≡ x
+    sym = ?
+    trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
+    trans = ?
+    cong : {A B : Set} {x y : A } { f : A → B } →   x ≡ y → f x ≡ f y
+    cong = ?
+
+</pre>
+
+<hr/>
+<h2><a name="content018">Ordering</a></h2>
+
+<p>
+Relation is a predicate on two value which has a same type.
+<p>
+
+<pre>
+   A → A → Set 
+
+</pre>
+Defining order is the definition of this type with predicate or a data.
+<p>
+
+<pre>
+    data _≤_ : Rel ℕ 0ℓ where
+      z≤n : ∀ {n}                 → zero  ≤ n
+      s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
+
+</pre>
+
+<hr/>
+<h2><a name="content019">Quantifier</a></h2>
+
+<p>
+Handling quantifier in an intuitionistic logic requires special cares.
+<p>
+In the input of a function, there are no restriction on it, that is, it has
+a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it)
+<p>
+There is no ∃ in agda, the one way is using negation like this.
+<p>
+ ∃ (x : A ) → p x  = ¬ ( ( x : A ) → ¬ ( p x ) )
+<p>
+On the another way, f : A can be used like this.
+<p>
+
+<pre>
+  p f
+
+</pre>
+If we use a function which can be defined globally which has stronger meaning the
+usage of ∃ x in a logical expression.
+<p>
+
+<hr/>
+<h2><a name="content020">Can we do math in this way?</a></h2>
+Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).
+<p>
+In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
+<p>
+
+<pre>
+    define mathematical structure as a record
+    program inferences as if we have proofs in variables
+
+</pre>
+
+<hr/>
+<h2><a name="content021">Things which Agda cannot prove</a></h2>
+
+<p>
+The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which
+leads uniqueness of a functor in Category Theory.
+<p>
+Functional extensionality cannot be proved.
+<pre>
+  (∀ x → f x ≡ g x) → f ≡ g
+
+</pre>
+Agda has no law of exclude middle.
+<p>
+
+<pre>
+  a ∨ ( ¬ a )
+
+</pre>
+For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot.
+<p>
+It also other problems such as termination, type inference or unification which we may overcome with
+efforts or devices or may not.
+<p>
+If we cannot prove something, we can safely postulate it unless it leads a contradiction.
+<pre>
+ 
+
+</pre>
+
+<hr/>
+<h2><a name="content022">Classical story of ZF Set Theory</a></h2>
+
+<p>
+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. 
+<p>
+In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
+We need some non constructive assumptions in the construction. A model of Set theory is
+constructed based on these assumptions.
+<p>
+<img src="fig/set-theory.svg">
+
+<p>
+
+<hr/>
+<h2><a name="content023">Ordinals</a></h2>
+Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
+It also has a successor osuc.
+<p>
+
+<pre>
+    record Ordinals {n : Level} : Set (suc (suc n)) where
+       field
+         ord : Set n
+         o∅ : ord
+         osuc : ord → ord
+         _o&lt;_ : ord → ord → Set n
+         isOrdinal : IsOrdinals ord o∅ osuc _o&lt;_
+
+</pre>
+It is different from natural numbers in way. The order of Ordinals is not defined in terms
+of successor. It is given from outside, which make it possible to have higher order infinity.
+<p>
+
+<hr/>
+<h2><a name="content024">Axiom of Ordinals</a></h2>
+Properties of infinite things. We request a transfinite induction, which states that if
+some properties are satisfied below all possible ordinals, the properties are true on all
+ordinals.
+<p>
+Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
+which is not a successor of any ordinals. It is called limit ordinal.
+<p>
+Any two ordinal can be compared, that is less, equal or more, that is total order.
+<p>
+
+<pre>
+  record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) 
+    (osuc : ord → ord )  
+    (_o&lt;_ : ord → ord → Set n) : Set (suc (suc n)) where
+   field
+     Otrans :  {x y z : ord }  → x o&lt; y → y o&lt; z → x o&lt; z
+     OTri : Trichotomous {n} _≡_  _o&lt;_ 
+     ¬x&lt;0 :   { x  : ord  } → ¬ ( x o&lt; o∅  )
+     &lt;-osuc :  { x : ord  } → x o&lt; osuc x
+     osuc-≡&lt; :  { a x : ord  } → x o&lt; osuc a  →  (x ≡ a ) ∨ (x o&lt; a)  
+     TransFinite : { ψ : ord  → Set (suc n) }
+          → ( (x : ord)  → ( (y : ord  ) → y o&lt; x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
+
+</pre>
+
+<hr/>
+<h2><a name="content025">Concrete Ordinals</a></h2>
+
+<p>
+We can define a list like structure with level, which is a kind of two dimensional infinite array.
+<p>
+
+<pre>
+    data OrdinalD {n : Level} :  (lv : Nat) → Set n where
+       Φ : (lv : Nat) → OrdinalD  lv
+       OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
+
+</pre>
+The order of the OrdinalD can be defined in this way.
+<p>
+
+<pre>
+    data _d&lt;_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
+       Φ&lt;  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d&lt; OSuc lx x
+       s&lt;  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d&lt; y  → OSuc  lx x d&lt; OSuc  lx y
+
+</pre>
+This is a simple data structure, it has no abstract assumptions, and it is countable many data
+structure.
+<p>
+
+<pre>
+   Φ 0
+   OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2)))
+   Osuc 0 (Φ 0) d&lt; Φ 1
+
+</pre>
+
+<hr/>
+<h2><a name="content026">Model of Ordinals</a></h2>
+
+<p>
+It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
+<p>
+So our Ordinals has a mode. This means axiom of Ordinals are consistent.
+<p>
+
+<hr/>
+<h2><a name="content027">Debugging axioms using Model</a></h2>
+Whether axiom is correct or not can be checked by a validity on a mode.
+<p>
+If not, we may fix the axioms or the model, such as the definitions of the order.
+<p>
+We can also ask whether the inputs exist.
+<p>
+
+<hr/>
+<h2><a name="content028">Countable Ordinals can contains uncountable set?</a></h2>
+Yes, the ordinals contains any level of infinite Set in the axioms.
+<p>
+If we handle real-number in the model, only countable number of real-number is used.
+<p>
+
+<pre>
+    from the outside view point, it is countable
+    from the internal view point, it is uncountable
+
+</pre>
+The definition of countable/uncountable is the same, but the properties are different
+depending on the context.
+<p>
+We don't show the definition of cardinal number here.
+<p>
+
+<hr/>
+<h2><a name="content029">What is Set</a></h2>
+The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
+<p>
+From naive point view, a set i a list, but in Agda, elements have all the same type.
+A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
+<p>
+Finite set may be written in finite series of ∨, but ...
+<p>
+
+<hr/>
+<h2><a name="content030">We don't ask the contents of Set. It can be anything.</a></h2>
+From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
+and all of them, and again we repeat this.
+<p>
+
+<pre>
+   φ {φ} {φ,{φ}}, {φ,{φ},...}
+
+</pre>
+It is called V.
+<p>
+This operation can be performed within a ZF Set theory. Classical Set Theory assumes
+ZF, so this kind of thing is allowed.
+<p>
+But in our case, we have no ZF theory, so we are going to use Ordinals.
+<p>
+
+<hr/>
+<h2><a name="content031">Ordinal Definable Set</a></h2>
+We can define a sbuset of Ordinals using predicates. What is a subset?
+<p>
+
+<pre>
+   a predicate has an Ordinal argument
+
+</pre>
+is an Ordinal Definable Set (OD). In Agda, OD is defined as follows.
+<p>
+
+<pre>
+    record OD : Set (suc n ) where
+      field
+        def : (x : Ordinal  ) → Set n
+
+</pre>
+Ordinals itself is not a set in a ZF Set theory but a class. In OD, 
+<p>
+
+<pre>
+   record { def = λ x → true }
+
+</pre>
+means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
+but we don't care about it.
+<p>
+
+<hr/>
+<h2><a name="content032">∋ in OD</a></h2>
+OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
+<p>
+
+<pre>
+      od→ord : OD  → Ordinal 
+
+</pre>
+we may check an OD 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 )
+
+</pre>
+In ψ : Ordinal → Set,  if A is a  record { def = λ x → ψ x } , then
+<p>
+
+<pre>
+    A x = def A ( od→ord x ) = ψ (od→ord x)
+
+</pre>
+
+<hr/>
+<h2><a name="content033">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="content034">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 / ∋ ).
+<p>
+
+<pre>
+     def y ( od→ord x )
+
+</pre>
+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.
+<p>
+
+<pre>
+  c&lt;→o&lt;  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o&lt; od→ord y
+
+</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, 
+<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.
+<p>
+<img src="fig/ODandOrdinals.svg">
+
+<p>
+
+<hr/>
+<h2><a name="content035">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="content036">Various Sets</a></h2>
+
+<p>
+In classical Set Theory, there is a hierarchy call L, which can be defined by a predicate.
+<p>
+
+<pre>
+    Ordinal / things satisfies axiom of Ordinal / extension of natural number 
+    V / hierarchical construction of Set from φ   
+    L / hierarchical predicate definable construction of Set from φ   
+    OD / equational formula on Ordinals 
+    Agda Set / Type / it also has a level
+
+</pre>
+
+<hr/>
+<h2><a name="content037">Fixes on ZF to intuitionistic logic</a></h2>
+
+<p>
+We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
+ZF axioms in Agda.
+<p>
+It may not valid in our model. We have to debug it.
+<p>
+Fixes are depends on axioms.
+<p>
+<img src="fig/axiom-type.svg">
+
+<p>
+<a href="fig/zf-record.html">
+ZFのrecord </a>
+<p>
+
+<hr/>
+<h2><a name="content038">Pure logical axioms</a></h2>
+
+<pre>
+   empty, pair, select, ε-inductioninfinity
+
+</pre>
+These are logical relations among OD.
+<p>
+
+<pre>
+     empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
+     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y ) 
+     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t 
+     selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
+     infinity∅ :  ∅ ∈ infinite
+     infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ( x , x ) ) ∈ infinite 
+     ε-induction : { ψ : OD  → Set (suc n)}
+       → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
+       → (x : OD ) → ψ x
+
+</pre>
+finitely can be define by Agda data.
+<p>
+
+<pre>
+    data infinite-d  : ( x : Ordinal  ) → Set n where
+        iφ :  infinite-d o∅
+        isuc : {x : Ordinal  } →   infinite-d  x  →
+                infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
+
+</pre>
+Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
+<p>
+
+<hr/>
+<h2><a name="content039">Axiom of Pair</a></h2>
+In the Tanaka's book, axiom of pair is as follows.
+<p>
+
+<pre>
+     ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
+
+</pre>
+We have fix ∃ z, a function (x , y) is defined, which is  _,_ .
+<p>
+
+<pre>
+     _,_ : ( A B : ZFSet  ) → ZFSet
+
+</pre>
+using this, we can define two directions in separates axioms, like this.
+<p>
+
+<pre>
+     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y ) 
+     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t 
+
+</pre>
+This is already written in Agda, so we use these as axioms. All inputs have ∀.
+<p>
+
+<hr/>
+<h2><a name="content040">pair in OD</a></h2>
+OD is an equation on Ordinals, we can simply write axiom of pair in the OD.
+<p>
+
+<pre>
+    _,_ : OD  → OD  → OD 
+    x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } 
+
+</pre>
+≡ is an equality of λ terms, but please not that this is equality on Ordinals.
+<p>
+
+<hr/>
+<h2><a name="content041">Validity of Axiom of Pair</a></h2>
+Assuming ZFSet is OD, we are going to prove pair→ .
+<p>
+
+<pre>
+    pair→ : ( x y t : OD  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y ) 
+    pair→ x y t p = ?
+
+</pre>
+In this program, type of p is ( x , y ) ∋ t , that is def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) .
+<p>
+Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
+<p>
+
+<pre>
+    pair→ x y t (case1 t≡x ) = ?
+    pair→ x y t (case2 t≡y ) = ?
+
+</pre>
+The type of the ? is ( t == x ) ∨ ( t == y ), again it is  data _∨_ .
+<p>
+
+<pre>
+    pair→ x y t (case1 t≡x ) = case1 ?
+    pair→ x y t (case2 t≡y ) = case2 ?
+
+</pre>
+The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
+which type is 
+<p>
+
+<pre>
+    t≡x : od→ord t ≡ od→ord x
+
+</pre>
+which is shown by an Agda command (C-C C-E : agda2-show-context ).
+<p>
+But we haven't defined == yet.
+<p>
+
+<hr/>
+<h2><a name="content042">Equality of OD and Axiom of Extensionality </a></h2>
+OD is defined by a predicates, if we compares normal form of the predicates, even if
+it contains the same elements, it may be different, which is no good as an equality of
+Sets.
+<p>
+Axiom of Extensionality requires sets having the same elements are handled in the same way
+each other.
+<p>
+
+<pre>
+    ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
+
+</pre>
+We can write this axiom in Agda as follows.
+<p>
+
+<pre>
+     extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
+
+</pre>
+So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show
+A ∈ w ⇔ B ∈ w from A == B.
+<p>
+x ==  y can be defined in this way.
+<p>
+
+<pre>
+    record _==_  ( a b :  OD  ) : Set n where
+      field
+         eq→ : ∀ { x : Ordinal  } → def a x → def b x
+         eq← : ∀ { x : Ordinal  } → def b x → def a x
+
+</pre>
+Actually, (z : OD) → (A ∋ z) ⇔ (B ∋ z) implies A == B.
+<p>
+
+<pre>
+    extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+    eq→ (extensionality0 {A} {B} eq ) {x} d = ?
+    eq← (extensionality0 {A} {B} eq ) {x} d = ?
+
+</pre>
+? are def B x and def A x and these are generated from  eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
+<p>
+Actual proof is rather complicated.
+<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
+
+</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
+
+</pre>
+
+<hr/>
+<h2><a name="content043">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
+<p>
+
+<pre>
+  ==→o≡ : { x y : OD  } → (x == 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)
+    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
+
+</pre>
+This assumption means we may have an equivalence set on any predicates.
+<p>
+
+<hr/>
+<h2><a name="content044">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
+
+</pre>
+
+<hr/>
+<h2><a name="content045">Axiom which have negation form</a></h2>
+
+<p>
+
+<pre>
+   Union, Selection
+
+</pre>
+These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )).
+<p>
+Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive.
+<p>
+Power Set axiom requires double negation, 
+<p>
+
+<pre>
+     power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  t ∋ x → ¬ ¬ ( A ∋ x ) 
+     power← : ∀( A t : ZFSet  ) → t ⊆_ A → Power A ∋ t 
+
+</pre>
+If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
+<p>
+
+<hr/>
+<h2><a name="content046">Union </a></h2>
+The original form of the Axiom of Union is
+<p>
+
+<pre>
+     ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
+
+</pre>
+Union requires the existence of b in  a ⊇ ∃ b ∋ x . We will use negation form of ∃.
+<p>
+
+<pre>
+     union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
+     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+
+</pre>
+The definition of Union in OD is like this.
+<p>
+
+<pre>
+    Union : OD  → OD   
+    Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
+
+</pre>
+Proof of validity is straight forward.
+<p>
+
+<pre>
+         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
+              ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
+         union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+         union← X z UX∋z =  FExists _ lemma UX∋z where
+              lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
+              lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
+
+</pre>
+where
+<p>
+
+<pre>
+        FExists : {m l : Level} → ( ψ : Ordinal  → Set m )
+          → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
+          → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
+          → ¬ p
+        FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
+
+</pre>
+which checks existence using contra-position.
+<p>
+
+<hr/>
+<h2><a name="content047">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>
+
+<pre>
+     ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
+
+</pre>
+The existential quantifier can be related by a function, 
+<p>
+
+<pre>
+     Replace : OD  → (OD  → OD  ) → OD
+
+</pre>
+The axioms becomes as follows.
+<p>
+
+<pre>
+     replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ
+     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
+
+</pre>
+In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has
+negation form of existential quantifier in the definition.
+<p>
+
+<pre>
+    in-codomain : (X : OD  ) → ( ψ : OD  → OD  ) → OD 
+    in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
+
+</pre>
+Besides this upper bounds is required.
+<p>
+
+<pre>
+    Replace : OD  → (OD  → OD  ) → OD 
+    Replace X ψ = record { def = λ x → (x o&lt; sup-o  ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+
+</pre>
+We omit the proof of the validity, but it is rather straight forward.
+<p>
+
+<hr/>
+<h2><a name="content048">Validity of Power Set Axiom</a></h2>
+The original Power Set Axiom is this.
+<p>
+
+<pre>
+     ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
+
+</pre>
+The existential quantifier is replaced by a function
+<p>
+
+<pre>
+    Power : ( A : OD  ) → OD
+
+</pre>
+t ⊆ X is a  record like this.
+<p>
+
+<pre>
+    record _⊆_ ( A B : OD   ) : Set (suc n) where
+      field
+         incl : { x : OD } → A ∋ x →  B ∋ x
+
+</pre>
+Axiom becomes likes this.
+<p>
+
+<pre>
+    power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+    power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+
+</pre>
+The validity of the axioms are slight complicated, we have to define set of all subset. We define
+subset in a different form.
+<p>
+
+<pre>
+    ZFSubset : (A x : OD  ) → OD 
+    ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
+
+</pre>
+We can prove, 
+<p>
+
+<pre>
+    ( {y : OD } → x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  ) 
+
+</pre>
+We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals,
+which is an Ordinals with our Model.
+<p>
+
+<pre>
+    Ord : ( a : Ordinal  ) → OD 
+    Ord  a = record { def = λ y → y o&lt; a }  
+    Def :  (A :  OD ) → OD 
+    Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+
+</pre>
+This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
+<p>
+
+<pre>
+    Power : OD  → OD 
+    Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
+
+</pre>
+Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
+<p>
+
+<pre>
+     ∩-≡ :  { a b : OD  } → ({x : OD  } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
+
+</pre>
+In case of Ord a  intro of Power Set axiom becomes valid.
+<p>
+
+<pre>
+    ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
+
+</pre>
+Using this, we can prove,
+<p>
+
+<pre>
+         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+         power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+
+</pre>
+
+<hr/>
+<h2><a name="content049">Axiom of regularity, Axiom of choice, ε-induction</a></h2>
+
+<p>
+Axiom of regularity requires non self intersectable elements (which is called minimum), if we
+replace it by a function, it becomes a choice function. It makes axiom of choice valid.
+<p>
+This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of
+choice also becomes valid.
+<p>
+
+<pre>
+  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD
+  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+
+</pre>
+We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
+Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
+<p>
+
+<pre>
+    ε-induction : { ψ : OD  → Set (suc n)}
+       → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
+       → (x : OD ) → ψ x
+
+</pre>
+In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals.
+<p>
+The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia.
+<p>
+
+<pre>
+     ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
+
+</pre>
+We can formulate like this.
+<p>
+
+<pre>
+     choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
+     choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
+
+</pre>
+It does not requires ∅ ∉ X .
+<p>
+
+<hr/>
+<h2><a name="content050">Axiom of choice and Law of Excluded Middle</a></h2>
+In our model, since OD 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.
+<p>
+Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
+perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the
+set is empty or not if we have an axiom of choice, so we have the law of the exclude middle  p ∨ ( ¬ p ) .
+<p>
+
+<pre>
+    ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
+    ppp  {p} {a} d = d
+
+</pre>
+We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
+and Law of Excluded Middle is equivalent in our mode.
+<p>
+
+<hr/>
+<h2><a name="content051">Relation-ship among ZF axiom</a></h2>
+<img src="fig/axiom-dependency.svg">
+
+<p>
+
+<hr/>
+<h2><a name="content052">Non constructive assumption in our model</a></h2>
+mapping between OD and Ordinals
+<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
+
+</pre>
+Equivalence on OD
+<p>
+
+<pre>
+  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+
+</pre>
+Upper bound
+<p>
+
+<pre>
+  sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal
+  sup-o&lt; :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o&lt;  sup-o ψ
+
+</pre>
+Axiom of choice and strong axiom of regularity.
+<p>
+
+<pre>
+  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD
+  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+
+</pre>
+
+<hr/>
+<h2><a name="content053">So it this correct?</a></h2>
+
+<p>
+Our axiom are syntactically the same in the text book, but negations are slightly different.
+<p>
+If we assumes excluded middle, these are exactly same.
+<p>
+Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
+<p>
+Except the upper bound, axioms are simple logical relation.
+<p>
+Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not.
+<p>
+Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts,
+but we don't have explicit upper limit on Ordinals.
+<p>
+Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
+<p>
+
+<hr/>
+<h2><a name="content054">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>
+Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
+these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
+<p>
+ZF record itself is not necessary, for example, topology theory without ZF can be possible.
+<p>
+
+<hr/>
+<h2><a name="content055">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>
+Topos itself is model of intuitionistic logic. 
+<p>
+Transitive Sets are objects of Cartesian closed category.
+It is possible to introduce Power Set Functor on it
+<p>
+We can use replacement A ∩ x for each element in Transitive Set,
+in the similar way of our power set axiom. I
+<p>
+A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus. 
+<p>
+Our Agda model is a proof theoretic version of it.
+<p>
+
+<hr/>
+<h2><a name="content056">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
+<p>
+definition of filter is not yet done
+<p>
+we may have a model without axiom of choice or without continuum hypothesis
+<p>
+Possible representation of continuum hypothesis is this.
+<p>
+
+<pre>
+     continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
+
+</pre>
+
+<hr/>
+<h2><a name="content057">Filter</a></h2>
+
+<p>
+filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
+is depends on axiom of choice.
+<p>
+
+<pre>
+    record Filter  ( L : OD  ) : Set (suc n) where
+       field
+           filter : OD
+           proper : ¬ ( filter ∋ od∅ )
+           inL :  filter ⊆ L 
+           filter1 : { p q : OD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+           filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
+
+</pre>
+We may construct a model of non standard analysis or set theory.
+<p>
+This may be simpler than classical forcing theory ( not yet done).
+<p>
+
+<hr/>
+<h2><a name="content058">Programming Mathematics</a></h2>
+Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
+structure are
+<p>
+
+<pre>
+   record and data
+
+</pre>
+Proof is check by type consistency not by the computation, but it may include some normalization.
+<p>
+Type inference and termination is not so clear in multi recursions.
+<p>
+Defining Agda record is a good way to understand mathematical theory, for examples,
+<p>
+
+<pre>
+    Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor )
+    Automaton ( Subset construction、Language containment)
+
+</pre>
+are proved in Agda.
+<p>
+
+<hr/>
+<h2><a name="content059">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
+</a>
+<p>
+Agda
+<br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">https://agda.readthedocs.io/en/v2.6.0.1/</a>
+<p>
+ZF-in-Agda source
+<br> <a href="https://github.com/shinji-kono/zf-in-agda.git">https://github.com/shinji-kono/zf-in-agda.git
+</a>
+<p>
+Category theory in Agda source
+<br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">https://github.com/shinji-kono/category-exercise-in-agda
+</a>
+<p>
+</div>
+<ol class="side" id="menu">
+Constructing ZF Set Theory in Agda 
+<li><a href="#content000">  Programming Mathematics</a>
+<li><a href="#content001">  Target</a>
+<li><a href="#content002">  Why Set Theory</a>
+<li><a href="#content003">  Agda and Intuitionistic Logic </a>
+<li><a href="#content004">  Introduction of Agda </a>
+<li><a href="#content005">  data ( Sum type )</a>
+<li><a href="#content006">   A → B means "A implies B"</a>
+<li><a href="#content007">  introduction と elimination</a>
+<li><a href="#content008">   To prove A → B </a>
+<li><a href="#content009">   A ∧ B</a>
+<li><a href="#content010">   record</a>
+<li><a href="#content011">   Mathematical structure</a>
+<li><a href="#content012">   A Model and a theory</a>
+<li><a href="#content013">   postulate と module</a>
+<li><a href="#content014">   A ∨ B</a>
+<li><a href="#content015">   Negation</a>
+<li><a href="#content016">  Equality </a>
+<li><a href="#content017">  Equivalence relation</a>
+<li><a href="#content018">  Ordering</a>
+<li><a href="#content019">  Quantifier</a>
+<li><a href="#content020">  Can we do math in this way?</a>
+<li><a href="#content021">  Things which Agda cannot prove</a>
+<li><a href="#content022">  Classical story of ZF Set Theory</a>
+<li><a href="#content023">  Ordinals</a>
+<li><a href="#content024">  Axiom of Ordinals</a>
+<li><a href="#content025">  Concrete Ordinals</a>
+<li><a href="#content026">  Model of Ordinals</a>
+<li><a href="#content027">  Debugging axioms using Model</a>
+<li><a href="#content028">  Countable Ordinals can contains uncountable set?</a>
+<li><a href="#content029">  What is Set</a>
+<li><a href="#content030">  We don't ask the contents of Set. It can be anything.</a>
+<li><a href="#content031">  Ordinal Definable Set</a>
+<li><a href="#content032">  ∋ in OD</a>
+<li><a href="#content033">  1 to 1 mapping between an OD and an Ordinal</a>
+<li><a href="#content034">  Order preserving in the mapping of OD and Ordinal</a>
+<li><a href="#content035">  ISO</a>
+<li><a href="#content036">  Various Sets</a>
+<li><a href="#content037">  Fixes on ZF to intuitionistic logic</a>
+<li><a href="#content038">  Pure logical axioms</a>
+<li><a href="#content039">  Axiom of Pair</a>
+<li><a href="#content040">  pair in OD</a>
+<li><a href="#content041">  Validity of Axiom of Pair</a>
+<li><a href="#content042">  Equality of OD and Axiom of Extensionality </a>
+<li><a href="#content043">  Validity of Axiom of Extensionality</a>
+<li><a href="#content044">  Non constructive assumptions so far</a>
+<li><a href="#content045">  Axiom which have negation form</a>
+<li><a href="#content046">  Union </a>
+<li><a href="#content047">  Axiom of replacement</a>
+<li><a href="#content048">  Validity of Power Set Axiom</a>
+<li><a href="#content049">  Axiom of regularity, Axiom of choice, ε-induction</a>
+<li><a href="#content050">  Axiom of choice and Law of Excluded Middle</a>
+<li><a href="#content051">  Relation-ship among ZF axiom</a>
+<li><a href="#content052">  Non constructive assumption in our model</a>
+<li><a href="#content053">  So it this correct?</a>
+<li><a href="#content054">  How to use Agda Set Theory</a>
+<li><a href="#content055">  Topos and Set Theory</a>
+<li><a href="#content056">  Cardinal number and Continuum hypothesis</a>
+<li><a href="#content057">  Filter</a>
+<li><a href="#content058">  Programming Mathematics</a>
+<li><a href="#content059">  link</a>
+</ol>
+
+<hr/>  Shinji KONO /  Sat Jan 11 20:04:01 2020
+</body></html>
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/zf-in-agda.ind	Sat Jan 11 20:11:51 2020 +0900
@@ -0,0 +1,1109 @@
+-title: Constructing ZF Set Theory in Agda 
+
+--author: Shinji KONO
+
+--Programming Mathematics
+
+Programming is processing data structure with λ terms.
+
+We are going to handle Mathematics in intuitionistic logic with λ terms.
+
+Mathematics is a functional programming which values are proofs.
+
+Programming ZF Set Theory in Agda
+
+--Target
+
+   Describe ZF axioms in Agda
+   Construction a Model of ZF Set Theory in Agda
+   Show necessary assumptions for the model
+   Show validities of ZF axioms on the model
+
+This shows consistency of Set Theory (with some assumptions),
+without circulating ZF Theory assumption.
+
+<a href="https://github.com/shinji-kono/zf-in-agda">
+ZF in Agda https://github.com/shinji-kono/zf-in-agda
+</a>
+
+--Why Set Theory
+
+If we can formulate Set theory, it suppose to work on any mathematical theory.
+
+Set Theory is a difficult point for beginners especially axiom of choice.
+
+It has some amount of difficulty and self circulating discussion.
+
+I'm planning to do it in my old age, but I'm enough age now.
+
+This is done during from May to September.
+
+--Agda and Intuitionistic Logic 
+
+Curry Howard Isomorphism
+
+    Proposition : Proof ⇔ Type : Value
+
+which means
+
+  constructing a typed lambda calculus which corresponds a logic
+
+Typed lambda calculus which allows complex type as a value of a variable (System FC)
+
+  First class Type / Dependent Type
+
+Agda is a such a programming language which has similar syntax of Haskell
+
+Coq is specialized in proof assistance such as command and tactics .
+
+--Introduction of Agda 
+
+A length of a list of type A.
+
+    length : {A : Set } → List A → Nat
+    length [] = zero
+    length (_ ∷ t)  = suc ( length t )
+
+Simple functional programming language. Type declaration is mandatory.
+A colon means type, an equal means value. Indentation based.
+
+Set is a base type (which may have a level ).
+
+{} means implicit variable which can be omitted if Agda infers its value.
+
+--data ( Sum type )
+
+A data type which as exclusive multiple constructors. A similar one as
+union in C or case class in Scala.
+
+It has a similar syntax as Haskell but it has a slight difference.
+
+   data List (A : Set ) : Set where
+        [] : List A
+        _∷_ : A → List A → List A
+
+_∷_ means infix operator. If use explicit _, it can be used in a normal function
+syntax.
+
+Natural number can be defined as a usual way.
+
+   data Nat : Set where
+        zero : Nat
+        suc  : Nat → Nat
+
+-- A → B means "A implies B"
+
+In Agda, a type can be a value of a variable, which is usually called dependent type.
+Type has a name Set in Agda.
+
+    ex3 : {A B : Set} → Set 
+    ex3 {A}{B}  =  A → B
+
+ex3 is a type : A → B, which is a value of Set. It also means a formula : A implies B.
+
+    A type is a formula, the value is the proof
+
+A value of A → B can be interpreted as an inference from the formula A to the formula B, which
+can be a function from a proof of A to a proof of B.
+
+--introduction と elimination
+
+For a logical operator, there are two types of inference, an introduction and an elimination.
+
+  intro creating symbol  / constructor / introduction
+  elim  using symbolic / accessors / elimination
+
+In Natural deduction, this can be written in proof schema.
+
+       A                   
+       :
+       B                    A       A → B
+   ------------- →intro   ------------------ →elim
+      A → B                     B
+
+In Agda, this is a pair of type and value as follows. Introduction of → uses λ.
+
+    →intro : {A B : Set } → A →  B → ( A → B )
+    →intro _ b = λ x → b
+
+    →elim : {A B : Set } → A → ( A → B ) → B
+    →elim a f = f a
+
+Important
+
+    {A B : Set } → A →  B → ( A → B )
+
+is
+
+    {A B : Set } → ( A →  ( B → ( A → B ) ))
+
+This makes currying of function easy.
+
+-- To prove A → B 
+
+Make a left type as an argument. (intros in Coq)
+
+    ex5 : {A B C : Set } → A → B → C  → ?
+    ex5 a b c = ?
+
+? is called a hole, which is unspecified part. Agda tell us which kind type is required for the Hole.
+
+We are going to fill the holes, and if we have no warnings nor errors such as type conflict (Red),
+insufficient proof or instance (Yellow), Non-termination, the proof is completed.
+
+-- A ∧ B
+
+Well known conjunction's introduction and elimination is as follow.
+
+     A    B                 A ∧ B           A ∧ B 
+   -------------         ----------- proj1   ---------- proj2
+      A ∧ B                   A               B
+
+We can introduce a corresponding structure in our functional programming language.
+
+-- record
+
+   record _∧_ A B : Set
+     field
+         proj1 : A
+         proj2 : B
+
+_∧_ means infix operator.  _∧_ A B can be written as  A ∧  B (Haskell uses (∧) )
+
+This a type which constructed from type A and type B. You may think this as an object
+or struct.
+
+   record { proj1 = x ; proj2 = y }    
+
+is a constructor of _∧_.
+
+    ex3 : {A B : Set} → A → B → ( A ∧ B )
+    ex3 a b = record { proj1 = a ; proj2 = b }
+
+    ex1 : {A B : Set} → ( A ∧ B ) → A
+    ex1 a∧b = proj1 a∧b
+
+a∧b is a variable name. If we have no spaces in a string, it is a word even if we have symbols
+except parenthesis or colons. A symbol requires space separation such as a type defining colon.
+
+Defining record can be recursively, but we don't use the recursion here.
+
+-- Mathematical structure
+
+We have types of elements and the relationship in a mathematical structure.
+
+  logical relation has no ordering
+  there is a natural ordering in arguments and a value in a function
+
+So we have typical definition style of mathematical structure with records.
+
+  record IsOrdinals {n : Level} (ord : Set n)  
+    (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
+   field
+     Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
+
+  record Ordinals {n : Level} : Set (suc (suc n)) where
+       field 
+         ord : Set n
+         _o<_ : ord → ord → Set n
+         isOrdinal : IsOrdinals ord _o<_
+
+In IsOrdinals, axioms are written in flat way. In Ordinal, we may have
+inputs and outputs are put in the field including IsOrdinal.
+
+Fields of Ordinal is existential objects in the mathematical structure.
+
+-- A Model and a theory
+
+Agda record is a type, so we can write it in the argument, but is it really exists?
+
+If we have a value of the record, it simply exists, that is, we need to create all the existence
+in the record satisfies all the axioms (= field of IsOrdinal) should be valid.
+
+   type of record = theory
+   value of record = model
+
+We call the value of the record as a model. If mathematical structure has a
+model, it exists. Pretty Obvious.
+
+-- postulate と module
+
+Agda proofs are separated by modules, which are large records.
+
+postulates are assumptions. We can assume a type without proofs.
+
+    postulate      
+      sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal 
+      sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o<  sup-o ψ 
+
+sup-o is an example of upper bound of a function and sup-o< assumes it actually 
+satisfies all the value is less than upper bound.
+
+Writing some type in a module argument is the same as postulating a type, but
+postulate can be written the middle of a proof.
+
+postulate can be constructive.
+
+postulate can be inconsistent, which result everything has a proof.
+
+-- A ∨ B
+
+    data _∨_ (A B : Set) : Set where
+      case1 : A → A ∨ B
+      case2 : B → A ∨ B
+
+As Haskell, case1/case2 are  patterns.
+
+    ex3 : {A B : Set} → ( A ∨ A ) → A 
+    ex3 = ?
+
+In a case statement, Agda command C-C C-C generates possible cases in the head.
+
+    ex3 : {A B : Set} → ( A ∨ A ) → A 
+    ex3 (case1 x) = ?
+    ex3 (case2 x) = ?
+
+Proof schema of ∨ is omit due to the complexity.
+
+-- Negation
+
+       ⊥
+    ------------- ⊥-elim
+       A
+
+Anything can be derived from bottom, in this case a Set A. There is no introduction rule
+in ⊥, which can be implemented as data which has no constructor.
+
+    data ⊥ : Set where
+
+⊥-elim can be proved like this.
+
+    ⊥-elim : {A : Set } -> ⊥ -> A
+    ⊥-elim ()
+
+() means no match argument nor value.
+
+A negation can be defined using ⊥ like this.
+
+    ¬_ : Set → Set
+    ¬ A = A → ⊥
+
+--Equality 
+
+All the value in Agda are terms. If we have the same normalized form, two terms are equal.
+If we have variables in the terms, we will perform an unification. unifiable terms are equal.
+We don't go further on the unification.
+
+     { x : A }                 x ≡ y    f x y
+   --------------- ≡-intro   --------------------- ≡-elim
+      x ≡ x                         f x x
+
+equality _≡_  can be defined as a data.
+
+    data _≡_ {A : Set } : A → A → Set where
+       refl :  {x : A} → x ≡ x
+
+The elimination of equality is a substitution in a term.
+
+    subst : {A : Set } → { x y : A } → ( f : A → Set ) → x ≡ y → f x → f y
+    subst {A} {x} {y} f refl fx = fx
+
+    ex5 :   {A : Set} {x y z : A } →  x ≡ y → y ≡ z → x ≡ z
+    ex5 {A} {x} {y} {z} x≡y y≡z = subst ( λ k → x ≡ k ) y≡z x≡y
+
+
+--Equivalence relation
+
+    refl' : {A : Set} {x : A } → x ≡ x
+    refl'  = ?
+    sym : {A : Set} {x y : A } → x ≡ y → y ≡ x
+    sym = ?
+    trans : {A : Set} {x y z : A } → x ≡ y → y ≡ z → x ≡ z
+    trans = ?
+    cong : {A B : Set} {x y : A } { f : A → B } →   x ≡ y → f x ≡ f y
+    cong = ?
+
+--Ordering
+
+Relation is a predicate on two value which has a same type.
+
+   A → A → Set 
+
+Defining order is the definition of this type with predicate or a data.
+
+    data _≤_ : Rel ℕ 0ℓ where
+      z≤n : ∀ {n}                 → zero  ≤ n
+      s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
+
+
+--Quantifier
+
+Handling quantifier in an intuitionistic logic requires special cares.
+
+In the input of a function, there are no restriction on it, that is, it has
+a universal quantifier. (If we explicitly write ∀, Agda gives us a type inference on it)
+
+There is no ∃ in agda, the one way is using negation like this.
+
+ ∃ (x : A ) → p x  = ¬ ( ( x : A ) → ¬ ( p x ) )
+
+On the another way, f : A can be used like this.
+
+  p f
+
+If we use a function which can be defined globally which has stronger meaning the
+usage of ∃ x in a logical expression.
+
+
+--Can we do math in this way?
+
+Yes, we can. Actually we have Principia Mathematica by Russell and Whitehead (with out computer support).
+
+In some sense, this story is a reprinting of the work, (but Principia Mathematica has a different formulation than ZF).
+
+    define mathematical structure as a record
+    program inferences as if we have proofs in variables
+
+--Things which Agda cannot prove
+
+The infamous Internal Parametricity is a limitation of Agda, it cannot prove so called Free Theorem, which
+leads uniqueness of a functor in Category Theory.
+
+Functional extensionality cannot be proved.
+  (∀ x → f x ≡ g x) → f ≡ g
+
+Agda has no law of exclude middle.
+
+  a ∨ ( ¬ a )
+
+For example, (A → B) → ¬ B → ¬ A can be proved but, ( ¬ B → ¬ A ) → A → B cannot.
+
+It also other problems such as termination, type inference or unification which we may overcome with
+efforts or devices or may not.
+
+If we cannot prove something, we can safely postulate it unless it leads a contradiction.
+ 
+--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. 
+
+In Agda, first we defines Ordinal numbers (Ordinals), then introduce Ordinal Definable Set (OD).
+We need some non constructive assumptions in the construction. A model of Set theory is
+constructed based on these assumptions.
+
+<center><img src="fig/set-theory.svg"></center>
+
+--Ordinals
+
+Ordinals are our intuition of infinite things, which has ∅ and orders on the things.
+It also has a successor osuc.
+
+    record Ordinals {n : Level} : Set (suc (suc n)) where
+       field
+         ord : Set n
+         o∅ : ord
+         osuc : ord → ord
+         _o<_ : ord → ord → Set n
+         isOrdinal : IsOrdinals ord o∅ osuc _o<_
+
+It is different from natural numbers in way. The order of Ordinals is not defined in terms
+of successor. It is given from outside, which make it possible to have higher order infinity.
+
+--Axiom of Ordinals
+
+Properties of infinite things. We request a transfinite induction, which states that if
+some properties are satisfied below all possible ordinals, the properties are true on all
+ordinals.
+
+Successor osuc has no ordinal between osuc and the base ordinal. There are some ordinals
+which is not a successor of any ordinals. It is called limit ordinal.
+
+Any two ordinal can be compared, that is less, equal or more, that is total order.
+
+  record IsOrdinals {n : Level} (ord : Set n)  (o∅ : ord ) 
+    (osuc : ord → ord )  
+    (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
+   field
+     Otrans :  {x y z : ord }  → x o< y → y o< z → x o< z
+     OTri : Trichotomous {n} _≡_  _o<_ 
+     ¬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)  
+     TransFinite : { ψ : ord  → Set (suc n) }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
+
+--Concrete Ordinals
+
+We can define a list like structure with level, which is a kind of two dimensional infinite array.
+
+    data OrdinalD {n : Level} :  (lv : Nat) → Set n where
+       Φ : (lv : Nat) → OrdinalD  lv
+       OSuc : (lv : Nat) → OrdinalD {n} lv → OrdinalD lv
+
+The order of the OrdinalD can be defined in this way.
+
+    data _d<_ {n : Level} :   {lx ly : Nat} → OrdinalD {n} lx  →  OrdinalD {n} ly  → Set n where
+       Φ<  : {lx : Nat} → {x : OrdinalD {n} lx}  →  Φ lx d< OSuc lx x
+       s<  : {lx : Nat} → {x y : OrdinalD {n} lx}  →  x d< y  → OSuc  lx x d< OSuc  lx y
+
+This is a simple data structure, it has no abstract assumptions, and it is countable many data
+structure.
+
+   Φ 0
+   OSuc 2 ( Osuc 2 ( Osuc 2 (Φ 2)))
+   Osuc 0 (Φ 0) d< Φ 1
+
+--Model of Ordinals
+
+It is easy to show OrdinalD and its order satisfies the axioms of Ordinals.
+
+So our Ordinals has a mode. This means axiom of Ordinals are consistent.
+
+--Debugging axioms using Model
+
+Whether axiom is correct or not can be checked by a validity on a mode.
+
+If not, we may fix the axioms or the model, such as the definitions of the order.
+
+We can also ask whether the inputs exist.
+
+--Countable Ordinals can contains uncountable set?
+
+Yes, the ordinals contains any level of infinite Set in the axioms.
+
+If we handle real-number in the model, only countable number of real-number is used.
+
+    from the outside view point, it is countable
+    from the internal view point, it is uncountable
+
+The definition of countable/uncountable is the same, but the properties are different
+depending on the context.
+
+We don't show the definition of cardinal number here.
+
+--What is Set
+
+The word Set in Agda is not a Set of ZF Set, but it is a type (why it is named Set?).
+
+From naive point view, a set i a list, but in Agda, elements have all the same type.
+A set in ZF may contain other Sets in ZF, which not easy to implement it as a list.
+
+Finite set may be written in finite series of ∨, but ...
+
+--We don't ask the contents of Set. It can be anything.
+
+From empty set φ, we can think a set contains a φ, and a pair of φ and the set, and so on,
+and all of them, and again we repeat this.
+
+   φ {φ} {φ,{φ}}, {φ,{φ},...}
+
+It is called V.
+
+This operation can be performed within a ZF Set theory. Classical Set Theory assumes
+ZF, so this kind of thing is allowed.
+
+But in our case, we have no ZF theory, so we are going to use Ordinals.
+
+
+--Ordinal Definable Set
+
+We can define a sbuset of Ordinals using predicates. What is a subset?
+
+   a predicate has an Ordinal argument
+
+is an Ordinal Definable Set (OD). In Agda, OD is defined as follows.
+
+    record OD : Set (suc n ) where
+      field
+        def : (x : Ordinal  ) → Set n
+
+Ordinals itself is not a set in a ZF Set theory but a class. In OD, 
+
+   record { def = λ x → true }
+
+means Ordinals itself, so ODs are larger than a notion of ZF Set Theory,
+but we don't care about it.
+
+
+--∋ in OD
+
+OD is a predicate on Ordinals and it does not contains OD directly. If we have a mapping
+
+      od→ord : OD  → Ordinal 
+
+we may check an OD 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 )
+
+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 / ∋ ).
+
+     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.
+
+  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
+
+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, 
+
+  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.
+
+<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.
+
+    Ordinal / things satisfies axiom of Ordinal / extension of natural number 
+    V / hierarchical construction of Set from φ   
+    L / hierarchical predicate definable construction of Set from φ   
+    OD / equational formula on Ordinals 
+    Agda Set / Type / it also has a level
+
+
+--Fixes on ZF to intuitionistic logic
+
+We use ODs as Sets in ZF, and defines record ZF, that is, we have to define
+ZF axioms in Agda.
+
+It may not valid in our model. We have to debug it.
+
+Fixes are depends on axioms.
+
+<center><img src="fig/axiom-type.svg"></center>
+
+<a href="fig/zf-record.html">
+ZFのrecord 
+</a>
+
+--Pure logical axioms
+
+   empty, pair, select, ε-inductioninfinity
+
+These are logical relations among OD.
+
+     empty :  ∀( x : ZFSet  ) → ¬ ( ∅ ∋ x )
+     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y ) 
+     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t 
+     selection : { ψ : ZFSet → Set m } → ∀ { X y : ZFSet  } →  ( ( y ∈ X ) ∧ ψ y ) ⇔ (y ∈  Select X ψ ) 
+     infinity∅ :  ∅ ∈ infinite
+     infinity :  ∀( x : ZFSet  ) → x ∈ infinite →  ( x ∪ ( x , x ) ) ∈ infinite 
+     ε-induction : { ψ : OD  → Set (suc n)}
+       → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
+       → (x : OD ) → ψ x
+
+finitely can be define by Agda data.
+
+    data infinite-d  : ( x : Ordinal  ) → Set n where
+        iφ :  infinite-d o∅
+        isuc : {x : Ordinal  } →   infinite-d  x  →
+                infinite-d  (od→ord ( Union (ord→od x , (ord→od x , ord→od x ) ) ))
+
+Union (x , ( x , x )) should be an direct successor of x, but we cannot prove it in our model.
+
+--Axiom of Pair
+
+In the Tanaka's book, axiom of pair is as follows.
+
+     ∀ x ∀ y ∃ z ∀ t ( z ∋ t ↔ t ≈ x ∨ t ≈ y)
+
+We have fix ∃ z, a function (x , y) is defined, which is  _,_ .
+
+     _,_ : ( A B : ZFSet  ) → ZFSet
+
+using this, we can define two directions in separates axioms, like this.
+
+     pair→ : ( x y t : ZFSet  ) →  (x , y)  ∋ t  → ( t ≈ x ) ∨ ( t ≈ y ) 
+     pair← : ( x y t : ZFSet  ) →  ( t ≈ x ) ∨ ( t ≈ y )  →  (x , y)  ∋ t 
+
+This is already written in Agda, so we use these as axioms. All inputs have ∀.
+
+--pair in OD
+
+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 ) } 
+
+≡ is an equality of λ terms, but please not that this is equality on Ordinals.
+
+--Validity of Axiom of Pair
+
+Assuming ZFSet is OD, we are going to prove pair→ .
+
+    pair→ : ( x y t : OD  ) →  (x , y)  ∋ t  → ( t == x ) ∨ ( t == y ) 
+    pair→ x y t p = ?
+
+In this program, type of p is ( x , y ) ∋ t , that is 
+def ( x , y ) that is, (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) .
+
+Since _∨_ is a data, it can be developed as (C-c C-c : agda2-make-case ).
+
+    pair→ x y t (case1 t≡x ) = ?
+    pair→ x y t (case2 t≡y ) = ?
+
+The type of the ? is ( t == x ) ∨ ( t == y ), again it is  data _∨_ .
+
+    pair→ x y t (case1 t≡x ) = case1 ?
+    pair→ x y t (case2 t≡y ) = case2 ?
+
+The ? in case1 is t == x, so we have to create this from t≡x, which is a name of a variable
+which type is 
+
+    t≡x : od→ord t ≡ od→ord x
+
+which is shown by an Agda command (C-C C-E : agda2-show-context ).
+
+But we haven't defined == yet.
+
+--Equality of OD and Axiom of Extensionality 
+
+OD is defined by a predicates, if we compares normal form of the predicates, even if
+it contains the same elements, it may be different, which is no good as an equality of
+Sets.
+
+Axiom of Extensionality requires sets having the same elements are handled in the same way
+each other.
+
+    ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
+
+We can write this axiom in Agda as follows.
+
+     extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
+
+So we use ( A ∋ z ) ⇔ (B ∋ z) as an equality (_==_) of our model. We have to show
+A ∈ w ⇔ B ∈ w from A == B.
+
+x ==  y can be defined in this way.
+
+    record _==_  ( a b :  OD  ) : Set n where
+      field
+         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.
+
+    extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
+    eq→ (extensionality0 {A} {B} eq ) {x} d = ?
+    eq← (extensionality0 {A} {B} eq ) {x} d = ?
+
+? are def B x and def A x and these are generated from  eq : (z : OD) → (A ∋ z) ⇔ (B ∋ z) .
+
+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
+
+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
+
+--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
+
+  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+
+Using this, we have
+
+    extensionality : {A B w : OD  } → ((z : OD ) → (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.
+
+--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
+
+
+--Axiom which have negation form
+
+   Union, Selection
+
+These axioms contains ∃ x as a logical relation, which can be described in ¬ ( ∀ x ( ¬ p )).
+
+Axiom of replacement uses upper bound of function on Ordinals, which makes it non-constructive.
+
+Power Set axiom requires double negation, 
+
+     power→ : ∀( A t : ZFSet  ) → Power A ∋ t → ∀ {x}  →  t ∋ x → ¬ ¬ ( A ∋ x ) 
+     power← : ∀( A t : ZFSet  ) → t ⊆_ A → Power A ∋ t 
+
+If we have an assumption of law of exclude middle, we can recover the original A ∋ x form.
+
+--Union 
+
+The original form of the Axiom of Union is
+
+     ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
+
+Union requires the existence of b in  a ⊇ ∃ b ∋ x . We will use negation form of ∃.
+
+     union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
+     union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) →  ¬  ( (u : ZFSet ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+
+The definition of Union in OD is like this.
+
+    Union : OD  → OD   
+    Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x)))  }
+
+Proof of validity is straight forward.
+
+         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx
+              ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } ))
+         union← :  (X z : OD) (X∋z : Union X ∋ z) →  ¬  ( (u : OD ) → ¬ ((X ∋  u) ∧ (u ∋ z )))
+         union← X z UX∋z =  FExists _ lemma UX∋z where
+              lemma : {y : Ordinal} → def X y ∧ def (ord→od y) (od→ord z) → ¬ ((u : OD) → ¬ (X ∋ u) ∧ (u ∋ z))
+              lemma {y} xx not = not (ord→od y) record { proj1 = subst ( λ k → def X k ) (sym diso) (proj1 xx ) ; proj2 = proj2 xx }
+
+where
+
+        FExists : {m l : Level} → ( ψ : Ordinal  → Set m )
+          → {p : Set l} ( P : { y : Ordinal  } →  ψ y → ¬ p )
+          → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
+          → ¬ p
+        FExists  {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
+
+which checks existence using contra-position.
+
+--Axiom of replacement
+
+We can replace the elements of a set by a function and it becomes a set. From the book, 
+
+     ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
+
+The existential quantifier can be related by a function, 
+
+     Replace : OD  → (OD  → OD  ) → OD
+
+The axioms becomes as follows.
+
+     replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ
+     replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
+
+In the axiom, the existence of the original elements is necessary. In order to do that we use OD which has
+negation form of existential quantifier in the definition.
+
+    in-codomain : (X : OD  ) → ( ψ : OD  → OD  ) → OD 
+    in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( def X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
+
+Besides this upper bounds is required.
+
+    Replace : OD  → (OD  → OD  ) → OD 
+    Replace X ψ = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+
+We omit the proof of the validity, but it is rather straight forward.
+
+--Validity of Power Set Axiom
+
+The original Power Set Axiom is this.
+
+     ∀ X ∃ A ∀ t ( t ∈ A ↔ t ⊆ X ) )
+
+The existential quantifier is replaced by a function
+
+    Power : ( A : OD  ) → OD
+
+t ⊆ X is a  record like this.
+
+    record _⊆_ ( A B : OD   ) : Set (suc n) where
+      field
+         incl : { x : OD } → A ∋ x →  B ∋ x
+
+Axiom becomes likes this.
+
+    power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+    power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+
+The validity of the axioms are slight complicated, we have to define set of all subset. We define
+subset in a different form.
+
+    ZFSubset : (A x : OD  ) → OD 
+    ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
+
+We can prove, 
+
+    ( {y : OD } → x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  ) 
+
+We only have upper bound as an ordinal, but we have an obvious OD based on the order of Ordinals,
+which is an Ordinals with our Model.
+
+    Ord : ( a : Ordinal  ) → OD 
+    Ord  a = record { def = λ y → y o< a }  
+
+    Def :  (A :  OD ) → OD 
+    Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+
+This is slight larger than Power A, so we replace all elements x by A ∩ x (some of them may empty).
+
+    Power : OD  → OD 
+    Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
+
+Creating Power Set of Ordinals is rather easy, then we use replacement axiom on A ∩ x since we have this.
+
+     ∩-≡ :  { a b : OD  } → ({x : OD  } → (a ∋ x → b ∋ x)) → a == ( b ∩ a )
+
+In case of Ord a  intro of Power Set axiom becomes valid.
+
+    ord-power← : (a : Ordinal ) (t : OD) → ({x : OD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
+
+Using this, we can prove,
+
+         power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
+         power← :  (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
+
+
+--Axiom of regularity, Axiom of choice, ε-induction
+
+Axiom of regularity requires non self intersectable elements (which is called minimum), if we
+replace it by a function, it becomes a choice function. It makes axiom of choice valid.
+
+This means we cannot prove axiom regularity form our model, and if we postulate this, axiom of
+choice also becomes valid.
+
+  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD
+  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+
+We can avoid this using ε-induction (a predicate is valid on all set if the predicate is true on some element of set).
+Assuming law of exclude middle, they say axiom of regularity will be proved, but we haven't check it yet.
+
+    ε-induction : { ψ : OD  → Set (suc n)}
+       → ( {x : OD } → ({ y : OD } →  x ∋ y → ψ y ) → ψ x )
+       → (x : OD ) → ψ x
+
+In our model, we assumes the mapping between Ordinals and OD, this is actually the TransFinite induction in Ordinals.
+
+The axiom of choice in the book is complicated using any pair in a set, so we use use a form in the Wikipedia.
+
+     ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
+
+We can formulate like this.
+
+     choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
+     choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
+
+It does not requires ∅ ∉ X .
+
+--Axiom of choice and Law of Excluded Middle
+
+In our model, since OD 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.
+
+Actually, it is well known to prove law of the exclude middle from axiom of choice in intuitionistic logic, and we can
+perform the proof in our mode. Using the definition like this, predicates and ODs are related and we can ask the
+set is empty or not if we have an axiom of choice, so we have the law of the exclude middle  p ∨ ( ¬ p ) .
+
+    ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
+    ppp  {p} {a} d = d
+
+We can prove axiom of choice from law excluded middle since we have TransFinite induction. So Axiom of choice
+and Law of Excluded Middle is equivalent in our mode.
+
+--Relation-ship among ZF axiom
+
+<center><img src="fig/axiom-dependency.svg"></center>
+
+--Non constructive assumption in our model
+
+mapping between OD and Ordinals
+
+  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
+
+Equivalence on OD
+
+  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+
+Upper bound
+
+  sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal
+  sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o<  sup-o ψ
+
+Axiom of choice and strong axiom of regularity.
+
+  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD
+  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+
+--So it this correct?
+
+Our axiom are syntactically the same in the text book, but negations are slightly different.
+
+If we assumes excluded middle, these are exactly same.
+
+Even if we assumes excluded middle, intuitionistic logic itself remains consistent, but we cannot prove it.
+
+Except the upper bound, axioms are simple logical relation.
+
+Proof of existence of mapping between OD and Ordinals are not obvious. We don't know we prove it or not.
+
+Existence of the Upper bounds is a pure assumption, if we have not limit on Ordinals, it may contradicts,
+but we don't have explicit upper limit on Ordinals.
+
+Several inference on our model or our axioms are basically parallel to the set theory text book, so it looks like correct.
+
+--How to use Agda Set Theory
+
+Assuming record ZF, classical set theory can be developed. If necessary, axiom of choice can be
+postulated or assuming law of excluded middle.
+
+Instead, simply assumes non constructive assumption, various theory can be developed. We haven't check
+these assumptions are proved in record ZF, so we are not sure, these development is a result of ZF Set theory.
+
+ZF record itself is not necessary, for example, topology theory without ZF can be possible.
+
+--Topos and Set Theory
+
+Topos is a mathematical structure in Category Theory, which is a Cartesian closed category which has a
+sub-object classifier. 
+
+Topos itself is model of intuitionistic logic. 
+
+Transitive Sets are objects of Cartesian closed category.
+It is possible to introduce Power Set Functor on it
+
+We can use replacement A ∩ x for each element in Transitive Set,
+in the similar way of our power set axiom. I
+
+A model of ZF Set theory can be constructed on top of the Topos which is shown in Oisus. 
+
+Our Agda model is a proof theoretic version of it.
+
+--Cardinal number and Continuum hypothesis
+
+Axiom of choice is required to define cardinal number
+
+definition of cardinal number is not yet done
+
+definition of filter is not yet done
+
+we may have a model without axiom of choice or without continuum hypothesis
+
+Possible representation of continuum hypothesis is this.
+
+     continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
+
+--Filter
+
+filter is a dual of ideal on boolean algebra or lattice. Existence on natural number
+is depends on axiom of choice.
+
+    record Filter  ( L : OD  ) : Set (suc n) where
+       field
+           filter : OD
+           proper : ¬ ( filter ∋ od∅ )
+           inL :  filter ⊆ L 
+           filter1 : { p q : OD } →  q ⊆ L  → filter ∋ p →  p ⊆ q  → filter ∋ q
+           filter2 : { p q : OD } → filter ∋ p →  filter ∋ q  → filter ∋ (p ∩ q)
+
+We may construct a model of non standard analysis or set theory.
+
+This may be simpler than classical forcing theory ( not yet done).
+
+--Programming Mathematics
+
+Mathematics is a functional programming in Agda where proof is a value of a variable. The mathematical
+structure are
+
+   record and data
+
+Proof is check by type consistency not by the computation, but it may include some normalization.
+
+Type inference and termination is not so clear in multi recursions.
+
+Defining Agda record is a good way to understand mathematical theory, for examples,
+
+    Category theory ( Yoneda lemma, Floyd Adjunction functor theorem, Applicative functor )
+    Automaton ( Subset construction、Language containment)
+
+are proved in Agda.
+
+--link
+
+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>
+
+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
+</a>
+
+Agda
+<br> <a href="https://agda.readthedocs.io/en/v2.6.0.1/">
+https://agda.readthedocs.io/en/v2.6.0.1/
+</a>
+
+ZF-in-Agda source
+<br> <a href="https://github.com/shinji-kono/zf-in-agda.git">
+https://github.com/shinji-kono/zf-in-agda.git
+</a>
+
+Category theory in Agda source
+<br> <a href="https://github.com/shinji-kono/category-exercise-in-agda">
+https://github.com/shinji-kono/category-exercise-in-agda
+</a>
+
+
+