# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1588984701 -32400
# Node ID d9d3654baee12c1b93a25a3994146bc001877b2b
# Parent  6f10c47e4e7a2b8df131734088bc08af287cc448
seperate choice from LEM

diff -r 6f10c47e4e7a -r d9d3654baee1 BAlgbra.agda
--- a/BAlgbra.agda	Sat May 09 09:02:52 2020 +0900
+++ b/BAlgbra.agda	Sat May 09 09:38:21 2020 +0900
@@ -18,6 +18,7 @@
 open inOrdinal O
 open OD O
 open OD.OD
+open ODAxiom odAxiom
 
 open _∧_
 open _∨_
diff -r 6f10c47e4e7a -r d9d3654baee1 LEMC.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/LEMC.agda	Sat May 09 09:38:21 2020 +0900
@@ -0,0 +1,87 @@
+open import Level
+open import Ordinals
+open import logic
+open import Relation.Nullary
+module LEMC {n : Level } (O : Ordinals {n} ) (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) 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.Binary
+open import Relation.Binary.Core
+
+open import nat
+import OD
+
+open inOrdinal O
+open OD O
+open OD.OD
+open OD._==_
+open ODAxiom odAxiom
+
+open import zfc
+
+--- 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
+
+open choiced
+
+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 = λ A {X} not A∋X → a-choice (choice-func X not );
+       choice = λ A {X} A∋X not → is-in (choice-func X not)
+     } where
+         choice-func :  (X : OD ) → ¬ ( X == od∅ ) → choiced X
+         choice-func  X 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 )
+                        }
+         
diff -r 6f10c47e4e7a -r d9d3654baee1 OD.agda
--- a/OD.agda	Sat May 09 09:02:52 2020 +0900
+++ b/OD.agda	Sat May 09 09:38:21 2020 +0900
@@ -52,6 +52,40 @@
 eq→ ( ⇔→==  {x} {y}  eq ) {z} m = proj1 eq m 
 eq← ( ⇔→==  {x} {y}  eq ) {z} m = proj2 eq m 
 
+-- next assumptions are our axiom
+--  it defines a subset of OD, which is called HOD, usually defined as
+--     HOD = { x | TC x ⊆ OD }
+--  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x
+
+record ODAxiom : Set (suc n) where      
+  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
+ field
+  od→ord : OD  → Ordinal 
+  ord→od : Ordinal  → OD  
+  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
+  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
+  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
+  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
+  -- 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 which we don't use
+  -- sup-x  : {n : Level } → ( OD → Ordinal ) →  Ordinal 
+  -- sup-lb : {n : Level } → { ψ : OD →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
+
+postulate  odAxiom : ODAxiom
+open ODAxiom odAxiom
+
+data One : Set n where
+  OneObj : One
+
+-- Ordinals in OD , the maximum
+Ords : OD
+Ords = record { def = λ x → One }
+
+maxod : {x : OD} → od→ord x o< od→ord Ords
+maxod {x} = c<→o< OneObj
+
 -- Ordinal in OD ( and ZFSet ) Transitive Set
 Ord : ( a : Ordinal  ) → OD 
 Ord  a = record { def = λ y → y o< a }  
@@ -59,37 +93,6 @@
 od∅ : OD  
 od∅  = Ord o∅ 
 
--- next assumptions are our axiom
---  it defines a subset of OD, which is called HOD, usually defined as
---     HOD = { x | TC x ⊆ OD }
---  where TC x is a transitive clusure of x, i.e. Union of all elemnts of all subset of x
-
-postulate      
-  -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
-  od→ord : OD  → Ordinal 
-  ord→od : Ordinal  → OD  
-  c<→o<  :  {x y : OD  }   → def y ( od→ord x ) → od→ord x o< od→ord y
-  oiso   :  {x : OD }      → ord→od ( od→ord x ) ≡ x
-  diso   :  {x : Ordinal } → od→ord ( ord→od x ) ≡ x
-  ==→o≡ : { x y : OD  } → (x == y) → x ≡ y
-  -- 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 ( 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 ψ))
-
-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
@@ -256,8 +259,8 @@
     A ∈ B = B ∋ A
     Power : OD  → OD 
     Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
-    ｛_｝ : ZFSet → ZFSet
-    ｛ x ｝ = ( x ,  x )
+    -- ｛_｝ : ZFSet → ZFSet
+    -- ｛ x ｝ = ( x ,  x )
 
     data infinite-d  : ( x : Ordinal  ) → Set n where
         iφ :  infinite-d o∅
diff -r 6f10c47e4e7a -r d9d3654baee1 ODC.agda
--- a/ODC.agda	Sat May 09 09:02:52 2020 +0900
+++ b/ODC.agda	Sat May 09 09:38:21 2020 +0900
@@ -19,6 +19,7 @@
 open OD O
 open OD.OD
 open OD._==_
+open ODAxiom odAxiom
 
 postulate      
   -- mimimul and x∋minimal is an Axiom of choice
diff -r 6f10c47e4e7a -r d9d3654baee1 OPair.agda
--- a/OPair.agda	Sat May 09 09:02:52 2020 +0900
+++ b/OPair.agda	Sat May 09 09:38:21 2020 +0900
@@ -17,6 +17,7 @@
 open inOrdinal O
 open OD O
 open OD.OD
+open ODAxiom odAxiom
 
 open _∧_
 open _∨_
diff -r 6f10c47e4e7a -r d9d3654baee1 cardinal.agda
--- a/cardinal.agda	Sat May 09 09:02:52 2020 +0900
+++ b/cardinal.agda	Sat May 09 09:38:21 2020 +0900
@@ -19,6 +19,7 @@
 open OD O
 open OD.OD
 open OPair O
+open ODAxiom odAxiom
 
 open _∧_
 open _∨_
diff -r 6f10c47e4e7a -r d9d3654baee1 filter.agda
--- a/filter.agda	Sat May 09 09:02:52 2020 +0900
+++ b/filter.agda	Sat May 09 09:38:21 2020 +0900
@@ -17,6 +17,7 @@
 open inOrdinal O
 open OD O
 open OD.OD
+open ODAxiom odAxiom
 
 open _∧_
 open _∨_