# HG changeset patch
# User Shinji KONO
# Date 1594103531 -32400
# Node ID de2c472bcbcd857655ab9015f4e6f5d636faf9b0
# Parent 231deb255e74be53e62098494612d0dd78425ce1
...
diff -r 231deb255e74 -r de2c472bcbcd README.md
--- a/README.md Mon Jul 06 17:14:46 2020 +0900
+++ b/README.md Tue Jul 07 15:32:11 2020 +0900
@@ -1,1 +1,111 @@
-zf-in-agda.ind
\ No newline at end of file
+Constructing ZF Set Theory in Agda
+============
+
+Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus
+
+## ZF in Agda
+
+```
+ zf.agda axiom of ZF
+ zfc.agda axiom of choice
+ Ordinals.agda axiom of Ordinals
+ ordinal.agda countable model of Ordinals
+ OD.agda model of ZF based on Ordinal Definable Set with assumptions
+ ODC.agda Law of exclude middle from axiom of choice assumptions
+ LEMC.agda model of choice with assumption of the Law of exclude middle
+ OPair.agda ordered pair on OD
+
+ BAlgbra.agda Boolean algebra on OD (not yet done)
+ filter.agda Filter on OD (not yet done)
+ cardinal.agda Caedinal number on OD (not yet done)
+
+ logic.agda some basics on logic
+ nat.agda some basics on Nat
+```
+
+## Ordinal Definable Set
+
+It is a predicate has an Ordinal argument.
+
+In Agda, OD is defined as follows.
+
+```
+ record OD : Set (suc n ) where
+ field
+ def : (x : Ordinal ) → Set n
+```
+
+This is not a ZF Set, because it can contain entire Ordinals.
+
+-- HOD : Hereditarily Ordinal Definable
+
+What we need is a bounded OD, the containment is limited by an ordinal.
+
+```
+ record HOD : Set (suc n) where
+ field
+ od : OD
+ odmax : Ordinal
+