changeset 276:6f10c47e4e7a

separate choice fix sup-o
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 09:02:52 +0900
parents 455792eaa611
children d9d3654baee1
files BAlgbra.agda OD.agda ODC.agda README.md cardinal.agda filter.agda ordinal.agda zf.agda zfc.agda
diffstat 9 files changed, 212 insertions(+), 203 deletions(-) [+]
line wrap: on
line diff
--- a/BAlgbra.agda	Sat Apr 25 15:09:17 2020 +0900
+++ b/BAlgbra.agda	Sat May 09 09:02:52 2020 +0900
@@ -5,6 +5,7 @@
 open import zf
 open import logic
 import OD 
+import ODC
 
 open import Relation.Nullary
 open import Relation.Binary
@@ -40,7 +41,7 @@
         lemma4 {y} z | case1 refl = double-neg (case1 ( subst (λ k → def k x ) oiso (proj2 z)) )
         lemma4 {y} z | case2 refl = double-neg (case2 ( subst (λ k → def k x ) oiso (proj2 z)) )
         lemma3 : (((u : Ordinals.ord O) → ¬ def (A , B) u ∧ def (ord→od u) x) → ⊥) → def (A ∪ B) x
-        lemma3 not = double-neg-eilm (FExists _ lemma4 not)   -- choice
+        lemma3 not = ODC.double-neg-eilm O (FExists _ lemma4 not)   -- choice
     lemma2 :  {x : Ordinal} → def (A ∪ B) x → def (Union (A , B)) x
     lemma2 {x} (case1 A∋x) = subst (λ k → def (Union (A , B)) k) diso ( IsZF.union→ isZF (A , B) (ord→od x) A
        (record { proj1 = case1 refl ; proj2 = subst (λ k → def A k) (sym diso) A∋x}))
--- a/OD.agda	Sat Apr 25 15:09:17 2020 +0900
+++ b/OD.agda	Sat May 09 09:02:52 2020 +0900
@@ -75,18 +75,21 @@
   -- next assumption causes ∀ x ∋ ∅ . It menas only an ordinal is allowed as OD
   --   o<→c<  : {n : Level} {x y : Ordinal  } → x o< y → def (ord→od y) x 
   --   ord→od x ≡ Ord x results the same
-  -- supermum as Replacement Axiom ( this assumes Ordinal has some upper bound )
-  sup-o  :  ( Ordinal  → Ordinal ) →  Ordinal 
-  sup-o< :  { ψ : Ordinal  →  Ordinal } → ∀ {x : Ordinal } → ψ x  o<  sup-o ψ 
+  -- supermum as Replacement Axiom ( corresponding Ordinal of OD has maximum )
+  sup-o  :  ( OD → Ordinal ) →  Ordinal 
+  sup-o< :  { ψ : OD →  Ordinal } → ∀ {x : OD } → ψ x  o<  sup-o ψ 
   -- contra-position of mimimulity of supermum required in Power Set Axiom
   -- sup-x  : {n : Level } → ( Ordinal  → Ordinal ) →  Ordinal 
   -- sup-lb : {n : Level } → { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
-  -- mimimul and x∋minimal is an Axiom of choice
-  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD 
-  -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
-  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
-  -- minimality (may proved by ε-induction )
-  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+
+data One : Set n where
+  OneObj : One
+
+Ords : OD
+Ords = record { def = λ x → One }
+
+maxod : {x : OD} → od→ord x o< od→ord Ords
+maxod {x} = c<→o< OneObj
 
 o<→c<→OD=Ord : ( {x y : Ordinal  } → x o< y → def (ord→od y) x ) → {x : OD } →  x ≡ Ord (od→ord x)
 o<→c<→OD=Ord o<→c< {x} = ==→o≡ ( record { eq→ = lemma1 ; eq← = lemma2 } ) where
@@ -108,12 +111,12 @@
 def-subst df refl refl = df
 
 sup-od : ( OD  → OD ) →  OD 
-sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
+sup-od ψ = Ord ( sup-o ( λ x → od→ord (ψ x)) )
 
 sup-c< :  ( ψ : OD  →  OD ) → ∀ {x : OD } → def ( sup-od ψ ) (od→ord ( ψ x ))
-sup-c<   ψ {x} = def-subst  {_} {_} {Ord ( sup-o  ( λ x → od→ord (ψ (ord→od x ))) )} {od→ord ( ψ x )}
+sup-c<   ψ {x} = def-subst  {_} {_} {Ord ( sup-o  ( λ x → od→ord (ψ x)) )} {od→ord ( ψ x )}
         lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
-    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
+    lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ x))
     lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst (sup-o< ) refl (sym diso)  )
 
 otrans : {n : Level} {a x y : Ordinal  } → def (Ord a) x → def (Ord x) y → def (Ord a) y
@@ -181,45 +184,6 @@
 _,_ : OD  → OD  → OD 
 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } --  Ord (omax (od→ord x) (od→ord y))
 
---
--- Axiom of choice in intutionistic logic implies the exclude middle
---     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
---
-
-ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
-ppp  {p} {a} d = d
-
-p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
-p∨¬p  p with is-o∅ ( od→ord ( record { def = λ x → p } ))
-p∨¬p  p | yes eq = case2 (¬p eq) where
-   ps = record { def = λ x → p }
-   lemma : ps == od∅ → p → ⊥
-   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq p0 )
-   ¬p : (od→ord ps ≡ o∅) → p → ⊥
-   ¬p eq = lemma ( subst₂ (λ j k → j ==  k ) oiso o∅≡od∅ ( o≡→== eq ))
-p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
-   ps = record { def = λ x → p }
-   eqo∅ : ps ==  od∅  → od→ord ps ≡  o∅  
-   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
-   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
-   lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
-
-decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
-decp  p with p∨¬p p
-decp  p | case1 x = yes x
-decp  p | case2 x = no x
-
-double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
-double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
-... | yes p = p
-... | no ¬p = ⊥-elim ( notnot ¬p )
-
-OrdP : ( x : Ordinal  ) ( y : OD  ) → Dec ( Ord x ∋ y )
-OrdP  x y with trio< x (od→ord y)
-OrdP  x y | tri< a ¬b ¬c = no ¬c
-OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
-OrdP  x y | tri> ¬a ¬b c = yes c
-
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
 
@@ -232,7 +196,7 @@
 ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  --   roughly x = A → Set 
 
 Def :  (A :  OD ) → OD 
-Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A x) ) )   
 
 -- _⊆_ :  ( A B : OD   ) → ∀{ x : OD  } →  Set n
 -- _⊆_ A B {x} = A ∋ x →  B ∋ x
@@ -283,7 +247,7 @@
     Select : (X : OD  ) → ((x : OD  ) → Set n ) → OD 
     Select X ψ = record { def = λ x →  ( def X x ∧ ψ ( ord→od x )) }
     Replace : OD  → (OD  → OD  ) → OD 
-    Replace X ψ = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
+    Replace X ψ = record { def = λ x → (x o< sup-o  ( λ x → od→ord (ψ x))) ∧ def (in-codomain X ψ) x }
     _∩_ : ( A B : ZFSet  ) → ZFSet
     A ∩ B = record { def = λ x → def A x ∧ def B x } 
     Union : OD  → OD   
@@ -406,7 +370,7 @@
               lemma1 :  {a : Ordinal } { t : OD }
                  → (eq : ZFSubset (Ord a) t == t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
               lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o  (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o  (λ x → od→ord (ZFSubset (Ord a) x))
               lemma = sup-o<  
 
          -- 
@@ -444,9 +408,9 @@
                  ≡⟨ sym (==→o≡ ( ∩-≡ t→A )) ⟩
                     t

-              lemma1 : od→ord t o< sup-o  (λ x → od→ord (A ∩ ord→od x))
-              lemma1 = subst (λ k → od→ord k o< sup-o   (λ x → od→ord (A ∩ ord→od x)))
-                  lemma4 (sup-o<  {λ x → od→ord (A ∩ ord→od x)} {od→ord t} )
+              lemma1 : od→ord t o< sup-o  (λ x → od→ord (A ∩ x))
+              lemma1 = subst (λ k → od→ord k o< sup-o   (λ x → od→ord (A ∩ x)))
+                  lemma4 (sup-o<  {λ x → od→ord (A ∩ x)}  )
               lemma2 :  def (in-codomain (Def (Ord (od→ord A))) (_∩_ A)) (od→ord t)
               lemma2 not = ⊥-elim ( not (od→ord t) (record { proj1 = lemma3 ; proj2 = lemma6 }) ) where
                   lemma6 : od→ord t ≡ od→ord (A ∩ ord→od (od→ord t)) 
@@ -459,21 +423,8 @@
                 lemma lt y<x | case1 refl = c<→o< y<x
                 lemma lt y<x | case2 x<a = ordtrans (c<→o< y<x) x<a 
 
-         -- continuum-hyphotheis : (a : Ordinal) → Power (Ord a) ⊆ Ord (osuc a)
-         -- continuum-hyphotheis a = ?
-
-         --  assuming axiom of choice
-         regularity :  (x : OD) (not : ¬ (x == od∅)) →
-            (x ∋ minimal x not) ∧ (Select (minimal x not) (λ x₁ → (minimal x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
-         proj1 (regularity x not ) = x∋minimal x not
-         proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where
-             lemma1 : {x₁ : Ordinal} → def (Select (minimal x not) (λ x₂ → (minimal x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁
-             lemma1 {x₁} s = ⊥-elim  ( minimal-1 x not (ord→od x₁) lemma3 ) where
-                 lemma3 : def (minimal x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁))
-                 lemma3 = record { proj1 = def-subst  {_} {_} {minimal x not} {_} (proj1 s) refl (sym diso)
-                                 ; proj2 = proj2 (proj2 s) } 
-             lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimal x not) (λ x₂ → (minimal x not ∋ x₂) ∧ (x ∋ x₂))) x₁
-             lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst  {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
+         continuum-hyphotheis : (a : Ordinal) → Set (suc n)
+         continuum-hyphotheis a = Power (Ord a) ⊆ Ord (osuc a)
 
          extensionality0 : {A B : OD } → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality0 {A} {B} eq ) {x} d = def-iso  {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
@@ -499,58 +450,6 @@
                     ≡ od→ord (Union (x , (x , x)))
                lemma = cong (λ k → od→ord (Union ( k , ( k , k ) ))) oiso 
 
-         -- Axiom of choice ( is equivalent to the existence of minimal in our case )
-         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
-         choice-func : (X : OD  ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
-         choice-func X {x} not X∋x = minimal x not
-         choice : (X : OD  ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
-         choice X {A} X∋A not = x∋minimal A not
-
-         ---
-         --- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
-         ---
-         record choiced  ( X : OD) : Set (suc n) where
-          field
-             a-choice : OD
-             is-in : X ∋ a-choice
-         
-         choice-func' :  (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
-         choice-func'  X p∨¬p not = have_to_find where
-                 ψ : ( ox : Ordinal ) → Set (suc n)
-                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
-                 lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite {ψ} induction ox where
-                    ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
-                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
-                    ∋-p A x | case1 (lift t)  = yes t
-                    ∋-p A x | case2 t  = no (λ x → t (lift x ))
-                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set (suc n) }
-                        → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
-                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
-                    ∀-imply-or  {A} {B} ∀AB | case1 (lift t) = case1 t
-                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x (lift not ))) where
-                         lemma : ¬ ((x : Ordinal ) → A x) →  B
-                         lemma not with p∨¬p B
-                         lemma not | case1 b = b
-                         lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
-                    induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
-                    induction x prev with ∋-p X ( ord→od x) 
-                    ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
-                    ... | no ¬p = lemma where
-                         lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
-                         lemma1 y with ∋-p X (ord→od y)
-                         lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
-                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
-                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
-                         lemma = ∀-imply-or lemma1
-                 have_to_find : choiced X
-                 have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
-                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
-                     ¬¬X∋x nn = not record {
-                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
-                          ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
-                        }
-         
 
 Union = ZF.Union OD→ZF
 Power = ZF.Power OD→ZF
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ODC.agda	Sat May 09 09:02:52 2020 +0900
@@ -0,0 +1,139 @@
+open import Level
+open import Ordinals
+module ODC {n : Level } (O : Ordinals {n} ) where
+
+open import zf
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+open import  Relation.Binary.PropositionalEquality
+open import Data.Nat.Properties 
+open import Data.Empty
+open import Relation.Nullary
+open import Relation.Binary
+open import Relation.Binary.Core
+
+open import logic
+open import nat
+import OD
+
+open inOrdinal O
+open OD O
+open OD.OD
+open OD._==_
+
+postulate      
+  -- mimimul and x∋minimal is an Axiom of choice
+  minimal : (x : OD  ) → ¬ (x == od∅ )→ OD 
+  -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
+  x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+  -- minimality (may proved by ε-induction )
+  minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+
+
+--
+-- Axiom of choice in intutionistic logic implies the exclude middle
+--     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
+--
+
+ppp :  { p : Set n } { a : OD  } → record { def = λ x → p } ∋ a → p
+ppp  {p} {a} d = d
+
+p∨¬p : ( p : Set n ) → p ∨ ( ¬ p )         -- assuming axiom of choice
+p∨¬p  p with is-o∅ ( od→ord ( record { def = λ x → p } ))
+p∨¬p  p | yes eq = case2 (¬p eq) where
+   ps = record { def = λ x → p }
+   lemma : ps == od∅ → p → ⊥
+   lemma eq p0 = ¬x<0  {od→ord ps} (eq→ eq p0 )
+   ¬p : (od→ord ps ≡ o∅) → p → ⊥
+   ¬p eq = lemma ( subst₂ (λ j k → j ==  k ) oiso o∅≡od∅ ( o≡→== eq ))
+p∨¬p  p | no ¬p = case1 (ppp  {p} {minimal ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
+   ps = record { def = λ x → p }
+   eqo∅ : ps ==  od∅  → od→ord ps ≡  o∅  
+   eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
+   lemma : ps ∋ minimal ps (λ eq →  ¬p (eqo∅ eq)) 
+   lemma = x∋minimal ps (λ eq →  ¬p (eqo∅ eq))
+
+decp : ( p : Set n ) → Dec p   -- assuming axiom of choice    
+decp  p with p∨¬p p
+decp  p | case1 x = yes x
+decp  p | case2 x = no x
+
+double-neg-eilm : {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
+double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
+... | yes p = p
+... | no ¬p = ⊥-elim ( notnot ¬p )
+
+OrdP : ( x : Ordinal  ) ( y : OD  ) → Dec ( Ord x ∋ y )
+OrdP  x y with trio< x (od→ord y)
+OrdP  x y | tri< a ¬b ¬c = no ¬c
+OrdP  x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
+OrdP  x y | tri> ¬a ¬b c = yes c
+
+open import zfc
+
+OD→ZFC : ZFC
+OD→ZFC   = record { 
+    ZFSet = OD 
+    ; _∋_ = _∋_ 
+    ; _≈_ = _==_ 
+    ; ∅  = od∅
+    ; Select = Select
+    ; isZFC = isZFC
+ } where
+    -- infixr  200 _∈_
+    -- infixr  230 _∩_ _∪_
+    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select 
+    isZFC = record {
+       choice-func = choice-func ;
+       choice = choice
+     } where
+         -- Axiom of choice ( is equivalent to the existence of minimal in our case )
+         -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] 
+         choice-func : (X : OD  ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
+         choice-func X {x} not X∋x = minimal x not
+         choice : (X : OD  ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A 
+         choice X {A} X∋A not = x∋minimal A not
+
+         --- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+         ---
+         record choiced  ( X : OD) : Set (suc n) where
+          field
+             a-choice : OD
+             is-in : X ∋ a-choice
+         
+         choice-func' :  (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
+         choice-func'  X p∨¬p not = have_to_find where
+                 ψ : ( ox : Ordinal ) → Set (suc n)
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
+                 lemma-ord : ( ox : Ordinal  ) → ψ ox
+                 lemma-ord  ox = TransFinite {ψ} induction ox where
+                    ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
+                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
+                    ∋-p A x | case1 (lift t)  = yes t
+                    ∋-p A x | case2 t  = no (λ x → t (lift x ))
+                    ∀-imply-or :  {A : Ordinal  → Set n } {B : Set (suc n) }
+                        → ((x : Ordinal ) → A x ∨ B) →  ((x : Ordinal ) → A x) ∨ B
+                    ∀-imply-or  {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
+                    ∀-imply-or  {A} {B} ∀AB | case1 (lift t) = case1 t
+                    ∀-imply-or  {A} {B} ∀AB | case2 x  = case2 (lemma (λ not → x (lift not ))) where
+                         lemma : ¬ ((x : Ordinal ) → A x) →  B
+                         lemma not with p∨¬p B
+                         lemma not | case1 b = b
+                         lemma not | case2 ¬b = ⊥-elim  (not (λ x → dont-orb (∀AB x) ¬b ))
+                    induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
+                    induction x prev with ∋-p X ( ord→od x) 
+                    ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
+                    ... | no ¬p = lemma where
+                         lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
+                         lemma1 y with ∋-p X (ord→od y)
+                         lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
+                         lemma = ∀-imply-or lemma1
+                 have_to_find : choiced X
+                 have_to_find = dont-or  (lemma-ord (od→ord X )) ¬¬X∋x where
+                     ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
+                     ¬¬X∋x nn = not record {
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
+                          ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
+                        }
+         
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/README.md	Sat May 09 09:02:52 2020 +0900
@@ -0,0 +1,1 @@
+zf-in-agda.ind
\ No newline at end of file
--- a/cardinal.agda	Sat Apr 25 15:09:17 2020 +0900
+++ b/cardinal.agda	Sat May 09 09:02:52 2020 +0900
@@ -5,6 +5,7 @@
 open import zf
 open import logic
 import OD 
+import ODC
 import OPair
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Relation.Binary.PropositionalEquality
@@ -29,7 +30,7 @@
 
     
 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
-∋-p A x with p∨¬p ( A ∋ x )
+∋-p A x with ODC.p∨¬p O ( A ∋ x )
 ∋-p A x | case1 t = yes t
 ∋-p A x | case2 t = no t
 
@@ -59,17 +60,17 @@
       func→od∈Func-1 :  Func dom cod ∋  func→od func-1 dom
  
 od→func : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f  → Func←cd {dom} {cod} {f} 
-od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
+od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x {!!} ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
    lemma : Ordinal → Ordinal → Ordinal
    lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
    lemma x y | p | no n  = o∅
-   lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
+   lemma x y | p | yes f∋y = lemma2 (proj1 (ODC.double-neg-eilm O ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
            lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
-           lemma2 (pair x1 y1) with decp ( x1 ≡ x)
+           lemma2 (pair x1 y1) with ODC.decp O ( x1 ≡ x)
            lemma2 (pair x1 y1) | yes p = y1
            lemma2 (pair x1 y1) | no ¬p = o∅
    fod : OD
-   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > )
+   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) {!!} )) > )
 
 
 open Func←cd
@@ -128,15 +129,15 @@
 
 cardinal :  (X  : OD ) → Cardinal X
 cardinal  X = record {
-       cardinal = sup-o ( λ x → proj1 ( cardinal-p x) )
+       cardinal = sup-o ( λ x → proj1 ( cardinal-p {!!}) )
      ; conto = onto
      ; cmax = cmax
    } where
     cardinal-p : (x  : Ordinal ) →  ( Ordinal  ∧ Dec (Onto X (Ord x) ) )
-    cardinal-p x with p∨¬p ( Onto X (Ord x)  ) 
+    cardinal-p x with ODC.p∨¬p O ( Onto X (Ord x)  ) 
     cardinal-p x | case1 True  = record { proj1 = x  ; proj2 = yes True }
     cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
-    S = sup-o (λ x → proj1 (cardinal-p x))
+    S = sup-o (λ x → proj1 (cardinal-p {!!}))
     lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) →
                     Lift (suc n) (x o< (osuc S) → Onto X (Ord x) )
     lemma1 x prev with trio< x (osuc S)
@@ -153,9 +154,9 @@
     ... | lift t = t <-osuc  
     cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y) 
     cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S}
-       (sup-o<  {λ x → proj1 ( cardinal-p x)}{y}  ) lemma refl ) where
+       (sup-o<  {λ x → proj1 ( cardinal-p {!!})}{{!!}}  ) lemma refl ) where
           lemma : proj1 (cardinal-p y) ≡ y
-          lemma with  p∨¬p ( Onto X (Ord y) )
+          lemma with  ODC.p∨¬p O ( Onto X (Ord y) )
           lemma | case1 x = refl
           lemma | case2 not = ⊥-elim ( not ontoy )
 
--- a/filter.agda	Sat Apr 25 15:09:17 2020 +0900
+++ b/filter.agda	Sat May 09 09:02:52 2020 +0900
@@ -81,7 +81,7 @@
 
    import ordinal
 
-   open  ordinal.C-Ordinal-with-choice 
+   -- open  ordinal.C-Ordinal-with-choice 
 
    Hω2 : Filter (Power (Power infinite))
    Hω2 = {!!}
--- a/ordinal.agda	Sat Apr 25 15:09:17 2020 +0900
+++ b/ordinal.agda	Sat May 09 09:02:52 2020 +0900
@@ -233,62 +233,3 @@
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
 
-module C-Ordinal-with-choice {n : Level} where
-
-  import OD 
-  -- open inOrdinal C-Ordinal 
-  open OD (C-Ordinal {n})
-  open OD.OD
-  open _⊆_
-
-  o<→c< :  {x y : Ordinal } → x o< y →   Ord x ⊆ Ord y 
-  o<→c< lt = record { incl = λ lt1 → ordtrans lt1 lt }
-
-  ⊆→o< :  {x y : Ordinal } →  Ord x ⊆ Ord y →  x o< osuc y
-  ⊆→o< {x} {y}  lt with trio< x y 
-  ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
-  ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
-  ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with incl lt  (o<-subst c (sym diso) refl )
-  ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
-
-  -- ZFSubset : (A x : OD  ) → OD 
-  -- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
-
-  -- Def :  (A :  OD ) → OD 
-  -- Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
-
-  Ord-lemma : (a : Ordinal)  →  ord→od a ⊆ Ord a
-  Ord-lemma a  = record { incl = λ lt → o<-subst (c<→o< lt ) refl diso }
-
-  ⊆-trans :  {a b c x : OD}  →  a ⊆ b  →   b ⊆ c  → a ⊆ c     
-  ⊆-trans a⊆b b⊆c = record { incl = λ a∋x →  incl b⊆c (incl a⊆b a∋x) }
-
-  _∩_ = IsZF._∩_ isZF
-
--- 
---   ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a)
---   ord-power-lemma {a} = record { eq→ = left ; eq← = right } where
---        left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x
---        left {x} lt = lemma1 where
---           lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y)))
---           lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} 
---           lemma1 : x o<  sup-o  ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) 
---           lemma1 = {!!}
---        right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x
---        right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso
--- 
---   uncountable : (a y : Ordinal) →  Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) 
---   uncountable a y = ⊆→o<  lemma  where
---        lemma-a :  (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x}
---        lemma-a x lt = proj1 lt
---        lemma :  (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x}
---        lemma x = {!!}
--- 
---   continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
---   continuum-hyphotheis a x = lemma2 where
---        lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a
---        lemma1 = {!!}
---        lemma : _⊆_ (Def (Ord a))  (Ord (osuc a)) {x}
---        lemma = o<→c< lemma1
---        lemma2 : _⊆_ (Power (Ord a))  (Ord (osuc a)) {x}
---        lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma
--- a/zf.agda	Sat Apr 25 15:09:17 2020 +0900
+++ b/zf.agda	Sat May 09 09:02:52 2020 +0900
@@ -48,11 +48,7 @@
      power← : ∀( A t : ZFSet  ) → ( ∀ {x}  →  _⊆_ t A {x})  → Power A ∋ t 
      -- extensionality : ∀ z ( z ∈ x ⇔ z ∈ y ) ⇒ ∀ w ( x ∈ w ⇔ y ∈ w )
      extensionality :  { A B w : ZFSet  } → ( (z : ZFSet) → ( A ∋ z ) ⇔ (B ∋ z)  ) → ( A ∈ w ⇔ B ∈ w )
-     -- This form of regurality forces choice function
-     -- regularity : ∀ x ( x ≠ ∅ → ∃ y ∈ x ( y ∩ x = ∅ ) )
-     -- minimal : (x : ZFSet ) → ¬ (x ≈ ∅) → ZFSet 
-     -- regularity : ∀( x : ZFSet  ) → (not : ¬ (x ≈ ∅)) → (  minimal x not  ∈ x ∧  (  minimal x not  ∩ x  ≈ ∅ ) )
-     -- another form of regularity
+     -- regularity without minimum
      ε-induction : { ψ : ZFSet → Set (suc m)}
               → ( {x : ZFSet } → ({ y : ZFSet } →  x ∋ y → ψ y ) → ψ x )
               → (x : ZFSet ) → ψ x
@@ -63,9 +59,6 @@
      -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) )
      replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) → x ∈ X → ψ x ∈  Replace X ψ 
      replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet  ) →  ( lt : x ∈  Replace X ψ ) → ¬ ( ∀ (y : ZFSet)  →  ¬ ( x ≈ ψ y ) )
-     -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
-     -- choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
-     -- choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
 
 record ZF {n m : Level } : Set (suc (n ⊔ suc m)) where
   infixr  210 _,_
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/zfc.agda	Sat May 09 09:02:52 2020 +0900
@@ -0,0 +1,34 @@
+module zfc where
+
+open import Level
+open import Relation.Binary
+open import Relation.Nullary
+open import logic
+
+record IsZFC {n m : Level }
+     (ZFSet : Set n)
+     (_∋_ : ( A x : ZFSet  ) → Set m)
+     (_≈_ : Rel ZFSet m)
+     (∅  : ZFSet)
+     (Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet ) 
+       : Set (suc (n ⊔ suc m)) where
+  field
+     -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
+     choice-func : (X : ZFSet ) → {x : ZFSet } → ¬ ( x ≈ ∅ ) → ( X ∋ x ) → ZFSet
+     choice : (X : ZFSet  ) → {A : ZFSet } → ( X∋A : X ∋ A ) → (not : ¬ ( A ≈ ∅ )) → A ∋ choice-func X not X∋A
+  infixr  200 _∈_
+  infixr  230 _∩_ 
+  _∈_ : ( A B : ZFSet  ) → Set m
+  A ∈ B = B ∋ A
+  _∩_ : ( A B : ZFSet  ) → ZFSet
+  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
+
+record ZFC {n m : Level } : Set (suc (n ⊔ suc m)) where
+  field
+     ZFSet : Set n
+     _∋_ : ( A x : ZFSet  ) → Set m 
+     _≈_ : ( A B : ZFSet  ) → Set m
+     ∅  : ZFSet
+     Select :  (X : ZFSet  ) → ( ψ : (x : ZFSet ) → Set m ) → ZFSet 
+     isZFC : IsZFC ZFSet _∋_ _≈_ ∅ Select
+