Constructing ZF Set Theory in Agda ============ Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus ## ZF in Agda [zfc](https://shinji-kono.github.io/zf-in-agda/html/zfc.html) axiom of choice [NSet](https://shinji-kono.github.io/zf-in-agda/html/NSet.html) Naive Set Theory [Ordinals](https://shinji-kono.github.io/zf-in-agda/html/Ordinals.html) axiom of Ordinals [OD](https://shinji-kono.github.io/zf-in-agda/html/OD.html) a model of ZF based on Ordinal Definable Set with assumptions [ODC](https://shinji-kono.github.io/zf-in-agda/html/ODC.html) Law of exclude middle from axiom of choice assumptions [LEMC](https://shinji-kono.github.io/zf-in-agda/html/LEMC.html) choice with assumption of the Law of exclude middle [BAlgebra](https://shinji-kono.github.io/zf-in-agda/html/BAlgebra.html) Boolean algebra on OD (not yet done) [zorn](https://shinji-kono.github.io/zf-in-agda/html/zorn.html) Zorn lemma [Topology](https://shinji-kono.github.io/zf-in-agda/html/Topology.html) Topology [Tychonoff](https://shinji-kono.github.io/zf-in-agda/html/Tychonoff.html) [VL](https://shinji-kono.github.io/zf-in-agda/html/VL.html) V and L [cardinal](https://shinji-kono.github.io/zf-in-agda/html/cardinal.html) Cardinals [filter](https://shinji-kono.github.io/zf-in-agda/html/filter.html) Filter [generic-filter](https://shinji-kono.github.io/zf-in-agda/html/generic-filter.html) Generic Filter [maximum-filter](https://shinji-kono.github.io/zf-in-agda/html/maximum-filter.html) Maximum filter by Zorn lemma [ordinal](https://shinji-kono.github.io/zf-in-agda/html/ordinal.html) countable model of Ordinals [OPair](https://shinji-kono.github.io/zf-in-agda/html/OPair.html) Orderd Pair and Direct Product ``` ## 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