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

comparison README.md @ 1200:42000f20fdbe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix README
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 01 Mar 2023 16:34:41 +0900
parents a5f8084b8368
children 003424a36fed
comparison
equal deleted inserted replaced
1199:1338b6c6a9b6 1200:42000f20fdbe
3 3
4 Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus 4 Shinji KONO (kono@ie.u-ryukyu.ac.jp), University of the Ryukyus
5 5
6 ## ZF in Agda 6 ## ZF in Agda
7 7
8 ``` 8 [zfc](https://shinji-kono.github.io/zf-in-agda/html/zfc.html) axiom of choice
9 zf.agda axiom of ZF
10 zfc.agda axiom of choice
11 Ordinals.agda axiom of Ordinals
12 ordinal.agda countable model of Ordinals
13 OD.agda model of ZF based on Ordinal Definable Set with assumptions
14 ODC.agda Law of exclude middle from axiom of choice assumptions
15 LEMC.agda model of choice with assumption of the Law of exclude middle
16 OPair.agda ordered pair on OD
17 9
18 BAlgbra.agda Boolean algebra on OD (not yet done) 10 [NSet](https://shinji-kono.github.io/zf-in-agda/html/NSet.html) Naive Set Theory
19 filter.agda Filter on OD (not yet done)
20 cardinal.agda Caedinal number on OD (not yet done)
21 11
22 logic.agda some basics on logic 12 [Ordinals](https://shinji-kono.github.io/zf-in-agda/html/Ordinals.html) axiom of Ordinals
23 nat.agda some basics on Nat 13
14 [OD](https://shinji-kono.github.io/zf-in-agda/html/OD.html) a model of ZF based on Ordinal Definable Set with assumptions
15
16 [ODC](https://shinji-kono.github.io/zf-in-agda/html/ODC.html) Law of exclude middle from axiom of choice assumptions
17
18 [LEMC](https://shinji-kono.github.io/zf-in-agda/html/LEMC.html) choice with assumption of the Law of exclude middle
19
20 [BAlgebra](https://shinji-kono.github.io/zf-in-agda/html/BAlgebra.html) Boolean algebra on OD (not yet done)
21
22 [zorn](https://shinji-kono.github.io/zf-in-agda/html/zorn.html) Zorn lemma
23
24 [Topology](https://shinji-kono.github.io/zf-in-agda/html/Topology.html) Topology
25
26 [Tychonoff](https://shinji-kono.github.io/zf-in-agda/html/Tychonoff.html)
27
28 [VL](https://shinji-kono.github.io/zf-in-agda/html/VL.html) V and L
29
30 [cardinal](https://shinji-kono.github.io/zf-in-agda/html/cardinal.html) Cardinals
31
32 [filter](https://shinji-kono.github.io/zf-in-agda/html/filter.html) Filter
33
34 [generic-filter](https://shinji-kono.github.io/zf-in-agda/html/generic-filter.html) Generic Filter
35
36 [maximum-filter](https://shinji-kono.github.io/zf-in-agda/html/maximum-filter.html) Maximum filter by Zorn lemma
37
38 [ordinal](https://shinji-kono.github.io/zf-in-agda/html/ordinal.html) countable model of Ordinals
39
40 [OPair](https://shinji-kono.github.io/zf-in-agda/html/OPair.html) Orderd Pair and Direct Product
41
42
24 ``` 43 ```
25 44
26 ## Ordinal Definable Set 45 ## Ordinal Definable Set
27 46
28 It is a predicate has an Ordinal argument. 47 It is a predicate has an Ordinal argument.