# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1671849570 -32400
# Node ID 40345abc0949f33f9c767338ccff10078adf188e
# Parent  55ab5de1ae02b522b0743148271e8c4d2a05c805
add README

diff -r 55ab5de1ae02 -r 40345abc0949 src/NSet.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/NSet.agda	Sat Dec 24 11:39:30 2022 +0900
@@ -0,0 +1,105 @@
+open import Level 
+module NSet (n : Level) where
+
+open import logic
+open import nat
+open import Data.Nat hiding (suc ; zero)
+open import Data.Nat.Properties
+open import Relation.Binary  hiding (_⇔_)
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+--
+-- Primitive Set on ℕ
+--
+
+record NSet : Set (suc zero) where
+   field
+      def : ℕ → Set 
+
+--
+-- Set as an equation on ℕ
+--
+eqa1 : NSet
+eqa1 = record { def = λ x →  x * x + 6 ≡ 5 * x   }
+
+open NSet
+
+_∋_ : NSet → ℕ → Set 
+S ∋ x = def S x
+
+eq1∋2 : eqa1 ∋ 2
+eq1∋2 = refl
+
+eq1∋3 : eqa1 ∋ 3
+eq1∋3 = refl
+
+--
+-- The solution
+--
+
+eqa2 : NSet
+eqa2 = record { def = λ x →  (x ≡ 2) ∨ ( x ≡ 3 )   }
+
+eq2∋3 : eqa2 ∋ 3
+eq2∋3 = case2 refl
+
+record _==_  ( a b :  NSet  ) : Set  where
+  field
+     eq→ : ∀ { x : ℕ } → def a x → def b x 
+     eq← : ∀ { x : ℕ } → def b x → def a x 
+
+_⊆_ : (a b : NSet ) → Set
+_⊆_ a b  = ∀ {x : ℕ} → def a x → def b x
+
+eq2⊆eq1 : eqa2 ⊆ eqa1
+eq2⊆eq1 {2} (case1 refl) = refl
+eq2⊆eq1 {3} (case2 refl) = refl
+
+-- the other way is slightly difficut
+
+data ⊥ : Set where                                          
+
+⊥-elim : {A : Set } → ⊥ →  A                                      
+⊥-elim ()                                          
+
+¬_ : Set → Set                                                                          
+¬ A = A → ⊥
+
+n∅ : NSet
+n∅  = record { def = λ y → y < 0 }        
+
+¬n∅∋x : {x : ℕ } → ¬ ( n∅ ∋ x  )
+¬n∅∋x ()
+
+¬n∅∋x' : {x : ℕ } → ¬ ( n∅ ∋ x  )
+¬n∅∋x' {x} nx = ⊥-elim ( n1 nx ) where
+   n1 : x < 0 → ⊥
+   n1 ()
+
+--
+-- Set of subset of ℕ
+--
+
+record NSetSet : Set (suc zero) where
+   field
+      ndef : NSet → Set 
+
+open NSetSet
+
+record _=n=_  ( a b :  NSetSet  ) : Set (suc zero) where
+  field
+     eq→ : ∀ { x : NSet } → ndef a x → ndef b x 
+     eq← : ∀ { x : NSet } → ndef b x → ndef a x 
+
+eqa3 : NSetSet
+eqa3 = record { ndef = λ x →  x == eqa2   }
+
+--
+--  Can we defined hierarchy of Set in monothic and consitent way?
+--     equations on Ordinal is an solution (Ordinal Definable Set)
+--     but we need some axioms to achive ZF Set Theory
+--
+
+
+
+
diff -r 55ab5de1ae02 -r 40345abc0949 src/OD.agda
--- a/src/OD.agda	Fri Dec 23 12:54:05 2022 +0900
+++ b/src/OD.agda	Sat Dec 24 11:39:30 2022 +0900
@@ -99,9 +99,9 @@
   *iso   :  {x : HOD }      → * ( & x ) ≡ x
   &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
-  sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal
+  sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal -- required in Replace
   sup-o≤ :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤  sup-o A ψ
--- possible order restriction
+-- possible order restriction (required in the axiom of infinite )
   ho< : {x : HOD} → & x o< next (odmax x)
 
 
@@ -402,12 +402,7 @@
 -- This means that many of OD may not be HODs because of the & mapping divergence.
 -- We should have some axioms to prevent this such as & x o< next (odmax x).
 --
--- postulate
---     ωmax : Ordinal
---     <ωmax : {y : Ordinal} → infinite-d y → y o< ωmax
---
--- infinite : HOD
--- infinite = record { od = record { def = λ x → infinite-d x } ; odmax = ωmax ; <odmax = <ωmax }
+--  Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
 
 infinite : HOD
 infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
diff -r 55ab5de1ae02 -r 40345abc0949 src/README.md
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/README.md	Sat Dec 24 11:39:30 2022 +0900
@@ -0,0 +1,117 @@
+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
+    zorn.agda          Zorn Lemma
+
+    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
+
+    NSet.agda          primitve set thoery examples
+
+    ODUtil.agda
+    OrdUtil.agda
+    PFOD.agda
+    Topology.agda
+    VL.agda
+    generic-filter.agda
+    partfunc.agda
+
+```
+
+## 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
+        <odmax : {y : Ordinal} → def od y → y o< odmax
+```
+
+In classical Set Theory, HOD stands for Hereditarily Ordinal Definable, which means
+
+```
+     HOD = { x | TC x ⊆ OD }
+```
+
+TC x is all transitive closure of x, that is elements of x and following all elements of them are all OD. But 
+what is x? In this case, x is an Set which we don't have yet. In our case, HOD is a bounded OD. 
+
+## 1 to 1 mapping between an HOD and an Ordinal
+
+HOD is a predicate on Ordinals and the solution is bounded by some ordinal. If we have a mapping
+
+```
+  od→ord : HOD  → Ordinal 
+  ord→od : Ordinal  → HOD  
+  oiso   :  {x : HOD }      → ord→od ( od→ord x ) ≡ x
+  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
+```
+
+we can check an HOD is an element of the OD using def.
+
+A ∋ x can be define as follows.
+
+```
+    _∋_ : ( A x : HOD  ) → Set n
+    _∋_  A x  = def (od 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)
+
+They say the existing of the mappings can be proved in Classical Set Theory, but we
+simply assumes these non constructively.
+
+## we need some more axiom to achive ZF Set Theory
+
+```
+    record ODAxiom : Set (suc n) where
+     field
+      -- HOD is isomorphic to Ordinal (by means of Goedel number)
+      & : HOD  → Ordinal
+      * : Ordinal  → HOD
+      c<→o<  :  {x y : HOD  }   → def (od y) ( & x ) → & x o< & y
+      ⊆→o≤   :  {y z : HOD  }   → ({x : Ordinal} → def (od y) x → def (od z) x ) → & y o< osuc (& z)
+      *iso   :  {x : HOD }      → * ( & x ) ≡ x
+      &iso   :  {x : Ordinal }  → & ( * x ) ≡ x
+      ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
+      sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal -- required in Replace
+      sup-o≤ :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤  sup-o A ψ
+    -- possible order restriction (required in the axiom of infinite )
+      ho< : {x : HOD} → & x o< next (odmax x)
+```
diff -r 55ab5de1ae02 -r 40345abc0949 src/zorn.agda
--- a/src/zorn.agda	Fri Dec 23 12:54:05 2022 +0900
+++ b/src/zorn.agda	Sat Dec 24 11:39:30 2022 +0900
@@ -243,6 +243,9 @@
 --
 --   Our Proof strategy of the Zorn Lemma  
 --
+--    As ZChain.cfcs closure of supf z is smaller than next supf z1, and supf z o< supfz1, because of mf<
+--    if have to be stopped since we have upper bound & A, so there is a Maximul element.
+--
 --         f (f ( ... (supf y))) f (f ( ... (supf z1)))
 --        /          |         /             |
 --       /           |        /              |
@@ -250,7 +253,6 @@
 --           o<                      o<
 --
 --    if sup z1 ≡ sup z2, the chain is stopped at sup z1, then f (sup z1) ≡ sup z1
---    this means sup z1 is the Maximal, so f is <-monotonic if we have no Maximal.
 --
 
 fc-stop : ( A : HOD )    ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) { a b : Ordinal }
@@ -312,9 +314,6 @@
    x≤sup = IsMinSUP.x≤sup isMinSUP
    minsup = IsMinSUP.minsup isMinSUP
 
-z09 : {b : Ordinal } { A : HOD } → odef A b → b o< & A
-z09 {b} {A} ab = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) ab))
-
 chain-mono : {A : HOD}  ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f )  {y : Ordinal} (ay : odef A y) (supf : Ordinal → Ordinal )
    (supf-mono : {x y : Ordinal } →  x o≤  y  → supf x o≤ supf y ) {a b c : Ordinal} → a o≤ b
         → odef (UnionCF A f ay supf a) c → odef (UnionCF A f ay supf b) c
@@ -326,11 +325,11 @@
    field
       supf :  Ordinal → Ordinal
 
+      asupf :  {x : Ordinal } → odef A (supf x)
+      is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
       supf-mono : {a b : Ordinal } → a o≤ b → supf a o≤ supf b
       cfcs  : {a b w : Ordinal } → a o< b → b o≤ z → supf a o< b → FClosure A f (supf a) w → odef (UnionCF A f ay supf b) w
-      asupf :  {x : Ordinal } → odef A (supf x)
-      zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x
-      is-minsup : {x : Ordinal } → (x≤z : x o≤ z) → IsMinSUP A (UnionCF A f ay supf x) (supf x)
+      zo≤sz : {x : Ordinal } → x o≤ z → x o≤ supf x   -- because of mf<
 
    chain : HOD
    chain = UnionCF A f ay supf z
@@ -357,7 +356,10 @@
    ... | case1 eq = ⊥-elim ( o<¬≡ (sym eq) sx<sy )
    ... | case2 lt = ⊥-elim ( o<> sx<sy lt )
 
-   csupf : {b : Ordinal } → supf b o< supf z → supf b o< z → odef (UnionCF A f ay supf z) (supf b) -- supf z is not an element of this chain
+   -- another kind of maximality of the chain
+   --    note that supf z is not an element of this chain
+   --
+   csupf : {b : Ordinal } → supf b o< supf z → supf b o< z → odef (UnionCF A f ay supf z) (supf b) 
    csupf {b} sb<sz sb<z = cfcs (supf-inject sb<sz) o≤-refl sb<z (init asupf refl)
 
    minsup : {x : Ordinal } → x o≤ z  → MinSUP A (UnionCF A f ay supf x)
@@ -390,6 +392,9 @@
            ... | tri≈ ¬a b ¬c = b
            ... | tri> ¬a ¬b b<sb = ⊥-elim ( o≤> z48 b<sb )
 
+   --
+   -- supf is minsup, so its UniofCF are equal, these are equal
+   -- 
    supfeq : {a b : Ordinal } → a o≤ z →  b o≤ z → UnionCF A f ay supf a ≡ UnionCF A f ay supf b → supf a ≡ supf b
    supfeq {a} {b} a≤z b≤z ua=ub with trio< (supf a) (supf b)
    ... | tri< sa<sb ¬b ¬c = ⊥-elim ( o≤> (
@@ -398,6 +403,9 @@
    ... | tri> ¬a ¬b sb<sa = ⊥-elim ( o≤> (
              IsMinSUP.minsup (is-minsup a≤z) asupf (λ {z} uza → IsMinSUP.x≤sup (is-minsup b≤z) (subst (λ k → odef k z) ua=ub uza)) ) sb<sa )
 
+   --
+   -- supf a over b and supf a is not included in UnionCF a nor UnionCF b, so UnionCF b is equal to the UnionCF a
+   --
    union-max : {a b : Ordinal } → b o≤ supf a → b o≤ z → supf a o< supf b → UnionCF A f ay supf a ≡ UnionCF A f ay supf b
    union-max {a} {b} b≤sa b≤z sa<sb = ==→o≡ record { eq→ = z47 ; eq← = z48 } where
           z47 : {w : Ordinal } → odef (UnionCF A f ay supf a ) w → odef ( UnionCF A f ay supf b ) w
@@ -613,7 +621,7 @@
                   ... | tri> ¬a ¬b s<z = ⊥-elim ( not s s<z ⟪ as , lt ⟫  )
                 ... | case2 notz = case1 (λ _ → notz )
          m03 : ¬ ((z : Ordinal) → z o< & A → ¬ odef A z ∧ xsup z)
-         m03 not = ⊥-elim ( not s1 (z09 (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where
+         m03 not = ⊥-elim ( not s1 (odef< (SUP.ax S)) ⟪ SUP.ax S , m05 ⟫ ) where
              S : SUP A B
              S = supP B  B⊆A total
              s1 = & (SUP.sup S)
@@ -682,9 +690,9 @@
                is-max {a} {b} ua b<x ab P a<b | case2 is-sup with osuc-≡< (ZChain.supf-mono zc (o<→≤ b<x))
                ... | case2 sb<sx = m10 where
                   b<A : b o< & A
-                  b<A = z09 ab
+                  b<A = odef< ab
                   m05 : ZChain.supf zc b ≡ b
-                  m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }
+                  m05 =  ZChain.sup=u zc ab (o<→≤ (odef< ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }
                   m10 : odef (UnionCF A f ay supf x) b
                   m10 = ZChain.cfcs zc b<x x≤A (subst (λ k → k o< x) (sym m05) b<x) (init (ZChain.asupf zc) m05)
                ... | case1 sb=sx = ⊥-elim (<-irr (case1 (cong (*) m10)) (proj1 (mf< (supf b) (ZChain.asupf zc)))) where
@@ -700,7 +708,7 @@
                           m04 nhp = proj1 is-sup ( record { ax = HasPrev.ax nhp ; y = HasPrev.y nhp ; ay =
                                 chain-mono1 (o<→≤ b<x) (HasPrev.ay  nhp) ; x=fy = HasPrev.x=fy nhp } )
                           m05 : ZChain.supf zc b ≡ b
-                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (odef< ab) )  record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz  }
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
@@ -732,7 +740,7 @@
                   m10 = fc-stop A f mf (ZChain.asupf zc) m11 sb=sx where
                       m11 : {z : Ordinal} → FClosure A f (supf b) z → (z ≡ ZChain.supf zc x) ∨ (z << ZChain.supf zc x)
                       m11 {z} fc = subst (λ k → (z ≡ k) ∨ (z << k)) (sym m18) ( MinSUP.x≤sup m17 m13 ) where
-                          m05 =  ZChain.sup=u zc ab (o<→≤ (z09 ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz }
+                          m05 =  ZChain.sup=u zc ab (o<→≤ (odef< ab) ) record { ax = ab ; x≤sup = λ {z} uz → IsSUP.x≤sup (proj2 is-sup) uz }
                           m14 : ZChain.supf zc b o< x
                           m14 = subst (λ k → k o< x ) (sym m05)  b<x
                           m13 :  odef (UnionCF A f ay supf x) z
@@ -802,7 +810,7 @@
                 ∨ (FClosure A f (supf0 px) z ∧ (supf0 px o< x)) } ; odmax = & A ; <odmax = zc00 } where
                zc00 : {z : Ordinal } → (odef A z ∧ UChain ay px z ) ∨ (FClosure A f (supf0 px) z ∧ (supf0 px o< x) )→ z o< & A
                zc00 {z} (case1 lt) = z07 lt
-               zc00 {z} (case2 fc) = z09 ( A∋fc (supf0 px) f mf (proj1 fc) )
+               zc00 {z} (case2 fc) = odef< ( A∋fc (supf0 px) f mf (proj1 fc) )
 
           zc02 : { a b : Ordinal } → odef A a ∧ UChain ay px a → FClosure A f (supf0 px) b ∧ ( supf0 px o< x) → a ≤ b
           zc02 {a} {b} ca fb = zc05 (proj1 fb) where
@@ -1241,7 +1249,7 @@
             ∨ (FClosure A f spu0 z ∧ (spu0 o< x)) } ; odmax = & A ; <odmax = zc00 } where
            zc00 : {z : Ordinal } → (odef A z ∧ IChain ay supfz z ) ∨ (FClosure A f spu0 z ∧ (spu0 o< x) )→ z o< & A
            zc00 {z} (case1 lt) = z07 lt
-           zc00 {z} (case2 fc) = z09 ( A∋fc spu0 f mf (proj1 fc) )
+           zc00 {z} (case2 fc) = odef< ( A∋fc spu0 f mf (proj1 fc) )
 
       zc02 : { a b : Ordinal } → odef A a ∧ IChain ay supfz a → FClosure A f spu0 b ∧ ( spu0 o< x) → a ≤ b
       zc02 {a} {b} ca fb = zc05 (proj1 fb) where
@@ -1518,11 +1526,11 @@
               → * a < * b  → odef chain b
            z10 = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl )
            z22 : sp o< & A
-           z22 = z09 asp
+           z22 = odef< asp
            z12 : odef chain sp
            z12 with o≡? (& s) sp
            ... | yes eq = subst (λ k → odef chain k) eq ( ZChain.chain∋init zc )
-           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (z09 asp) asp (case2 z19 ) z13 where
+           ... | no ne = ZChain1.is-max (SZ1 f mf mf< as0 zc (& A) o≤-refl) {& s} {sp} ( ZChain.chain∋init zc ) (odef< asp) asp (case2 z19 ) z13 where
                z13 :  * (& s) < * sp
                z13 with MinSUP.x≤sup sp1 ( ZChain.chain∋init zc )
                ... | case1 eq = ⊥-elim ( ne eq )