# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1593931740 -32400
# Node ID 0faa7120e4b53628ceac48f66bfdddc959184ada
# Parent  5544f4921a44931faa63656f23dfff1db00587ea
...

diff -r 5544f4921a44 -r 0faa7120e4b5 LEMC.agda
--- a/LEMC.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/LEMC.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -23,38 +23,42 @@
 
 open import zfc
 
---- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+--- With assuption of HOD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
 ---
-record choiced  ( X : OD) : Set (suc n) where
+record choiced  ( X : HOD) : Set (suc n) where
   field
-     a-choice : OD
+     a-choice : HOD
      is-in : X ∋ a-choice
 
+open HOD
+_=h=_ : (x y : HOD) → Set n
+x =h= y  = od x == od y
+
 open choiced
 
 OD→ZFC : ZFC
 OD→ZFC   = record { 
-    ZFSet = OD 
+    ZFSet = HOD 
     ; _∋_ = _∋_ 
-    ; _≈_ = _==_ 
+    ; _≈_ = _=h=_ 
     ; ∅  = od∅
     ; Select = Select
     ; isZFC = isZFC
  } where
     -- infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
-    isZFC : IsZFC (OD )  _∋_  _==_ od∅ Select 
+    isZFC : IsZFC (HOD )  _∋_  _=h=_ 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 : HOD ) → ¬ ( X =h= 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
+                 ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ odef X x )) ∨ choiced X
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = TransFinite {ψ} induction ox where
-                    ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
+                 lemma-ord  ox = TransFinite1 {ψ} induction ox where
+                    ∋-p : (A x : HOD ) → 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 ))
@@ -71,59 +75,61 @@
                     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 : Ordinal) → (y o< x → odef 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
+                         lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → odef X k ) (sym diso) y<X ) )
+                         lemma :  ((y : Ordinals.ord O) → (O Ordinals.o< y) x → odef 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 : ¬ ((x : Ordinal) → x o< (od→ord X) → odef X x → ⊥)
                      ¬¬X∋x nn = not record {
-                            eq→ = λ {x} lt → ⊥-elim  (nn x (def→o< lt) lt) 
+                            eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                         }
-         record Minimal (x : OD)  : Set (suc n) where
+         record Minimal (x : HOD)  : Set (suc n) where
            field
-               min : OD
+               min : HOD
                x∋min :   x ∋ min 
-               min-empty :  (y : OD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
+               min-empty :  (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
          open Minimal
          open _∧_
          --
          --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
          --
-         induction : {x : OD} → ({y : OD} → x ∋ y → (u : OD ) → (u∋x : u ∋ y) → Minimal u )
-              →  (u : OD ) → (u∋x : u ∋ x) → Minimal u 
-         induction {x} prev u u∋x with p∨¬p ((y : OD) → ¬ (x ∋ y) ∧ (u ∋ y))
+         induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
+              →  (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
+         induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
          ... | case1 P =
               record { min = x
                 ;     x∋min = u∋x
                 ;     min-empty = P
               } 
          ... | case2 NP =  min2 where
-              p : OD
-              p  = record { def = λ y1 → def x  y1 ∧ def u y1 }
-              np : ¬ (p == od∅)
+              p : HOD
+              p  = record { od = record { def = λ y1 → odef x  y1 ∧ odef u y1 } ; odmax = omin (odmax x) (odmax u) ; <odmax = lemma } where
+                 lemma : {y : Ordinal} → OD.def (od x) y ∧ OD.def (od u) y → y o< omin (odmax x) (odmax u)
+                 lemma {y} lt = min1 (<odmax x (proj1 lt)) (<odmax u (proj2 lt))
+              np : ¬ (p =h= od∅)
               np p∅ =  NP (λ y p∋y → ∅< p∋y p∅ ) 
               y1choice : choiced p
               y1choice = choice-func p np
-              y1 : OD
+              y1 : HOD
               y1 = a-choice y1choice
               y1prop : (x ∋ y1) ∧ (u ∋ y1)
               y1prop = is-in y1choice
               min2 : Minimal u
               min2 = prev (proj1 y1prop) u (proj2 y1prop)
-         Min2 : (x : OD) → (u : OD ) → (u∋x : u ∋ x) → Minimal u 
-         Min2 x u u∋x = (ε-induction {λ y →  (u : OD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
-         cx : {x : OD} →  ¬ (x == od∅ ) → choiced x 
+         Min2 : (x : HOD) → (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
+         Min2 x u u∋x = (ε-induction1 {λ y →  (u : HOD ) → (u∋x : u ∋ y) → Minimal u  } induction x u u∋x ) 
+         cx : {x : HOD} →  ¬ (x =h= od∅ ) → choiced x 
          cx {x} nx = choice-func x nx
-         minimal : (x : OD  ) → ¬ (x == od∅ ) → OD 
+         minimal : (x : HOD  ) → ¬ (x =h= od∅ ) → HOD 
          minimal x not = min (Min2 (a-choice (cx not) ) x (is-in (cx not))) 
-         x∋minimal : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
+         x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
          x∋minimal x ne = x∋min (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) 
-         minimal-1 : (x : OD  ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord  y) )
+         minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
          minimal-1 x ne y = min-empty (Min2 (a-choice (cx ne) ) x (is-in (cx ne))) y
 
 
diff -r 5544f4921a44 -r 0faa7120e4b5 OD.agda
--- a/OD.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/OD.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -260,6 +260,15 @@
      ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
      ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
 
+ε-induction1 : { ψ : HOD  → Set (suc n)}
+   → ( {x : HOD } → ({ y : HOD } →  x ∋ y → ψ y ) → ψ x )
+   → (x : HOD ) → ψ x
+ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc )  where
+     induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
+     induction ox prev = ind  ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 
+     ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
+     ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
+
 HOD→ZF : ZF  
 HOD→ZF   = record { 
     ZFSet = HOD 
diff -r 5544f4921a44 -r 0faa7120e4b5 ODC.agda
--- a/ODC.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/ODC.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -31,7 +31,7 @@
   minimal : (x : HOD  ) → ¬ (x =h= od∅ )→ HOD 
   -- this should be ¬ (x =h= od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimal : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → odef x ( od→ord ( minimal x ne ) )
-  -- minimality (may proved by ε-induction )
+  -- minimality (may proved by ε-induction with LEM)
   minimal-1 : (x : HOD  ) → ( ne : ¬ (x =h= od∅ ) ) → (y : HOD ) → ¬ ( odef (minimal x ne) (od→ord y)) ∧ (odef x (od→ord  y) )
 
 
@@ -40,8 +40,8 @@
 --     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
 --
 
--- ppp :  { p : Set n } { a : HOD  } → record { def = λ x → p } ∋ a → p
--- ppp  {p} {a} d = d
+ppp :  { p : Set n } { a : HOD  } → record { od = record { def = λ x → p } ; odmax = {!!} ; <odmax = {!!} } ∋ 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 { odef = λ x → p } ))
diff -r 5544f4921a44 -r 0faa7120e4b5 Ordinals.agda
--- a/Ordinals.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/Ordinals.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -25,6 +25,9 @@
      TransFinite : { ψ : ord  → Set n }
           → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
           →  ∀ (x : ord)  → ψ x
+     TransFinite1 : { ψ : ord  → Set (suc n) }
+          → ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord)  → ψ x
 
 
 record Ordinals {n : Level} : Set (suc (suc n)) where
@@ -57,6 +60,7 @@
         osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
         TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
+        TransFinite1 = IsOrdinals.TransFinite1  (Ordinals.isOrdinal O)
         next-limit = IsOrdinals.next-limit  (Ordinals.isOrdinal O)
 
         o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
diff -r 5544f4921a44 -r 0faa7120e4b5 ordinal.agda
--- a/ordinal.agda	Sun Jul 05 12:32:09 2020 +0900
+++ b/ordinal.agda	Sun Jul 05 15:49:00 2020 +0900
@@ -219,6 +219,7 @@
      ; <-osuc = <-osuc
      ; osuc-≡< = osuc-≡<
      ; TransFinite = TransFinite1
+     ; TransFinite1 = TransFinite2
      ; not-limit = not-limit
      ; next-limit = next-limit
    }
@@ -244,4 +245,15 @@
         caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
+     TransFinite2 : { ψ : ord1  → Set (suc (suc n)) }
+          → ( (x : ord1)  → ( (y : ord1  ) → y o< x → ψ y ) → ψ x )
+          →  ∀ (x : ord1)  → ψ x
+     TransFinite2 {ψ} lt x = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc x where
+        caseΦ : (lx : Nat) → ((x₁ : Ordinal) → x₁ o< ordinal lx (Φ lx) → ψ x₁) →
+            ψ (record { lv = lx ; ord = Φ lx })
+        caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
+        caseOSuc :  (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
+            ψ (record { lv = lx ; ord = OSuc lx x₁ })
+        caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
 
+