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

changeset 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 1338b6c6a9b6
children 03684784bc5f
files README.md src/Tychonoff.agda src/generic-filter.agda
diffstat 3 files changed, 35 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/README.md	Wed Mar 01 10:42:05 2023 +0900
+++ b/README.md	Wed Mar 01 16:34:41 2023 +0900
@@ -5,22 +5,41 @@
 
 ## 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
+[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
 
-    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)
+[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
 
-    logic.agda         some basics on logic
-    nat.agda           some basics on Nat
+[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
--- a/src/Tychonoff.agda	Wed Mar 01 10:42:05 2023 +0900
+++ b/src/Tychonoff.agda	Wed Mar 01 16:34:41 2023 +0900
@@ -66,7 +66,7 @@
    -- P is empty
    fip02 : {x : Ordinal } → ¬ odef P x
    fip02 {x} Px = ⊥-elim ( o<¬≡ (sym b) (∈∅< Px) )
-... | tri> ¬a ¬b 0<P = record { limit = limit ; is-limit = uf01 } where
+... | tri> ¬a ¬b 0<P = record { limit = ? ; is-limit = uf01 } where
      fip : {X : Ordinal} → * X ⊆ CS TP → Set n
      fip {X} CSX = {x : Ordinal} → Subbase (* X) x → o∅ o< x
      N : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip CSX → HOD
--- a/src/generic-filter.agda	Wed Mar 01 10:42:05 2023 +0900
+++ b/src/generic-filter.agda	Wed Mar 01 16:34:41 2023 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 open import Ordinals
 module generic-filter {n : Level } (O : Ordinals {n})   where