# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565702470 -32400
# Node ID e06b76e5b6827904b89ba2540c4186d9e9c2d5dc
# Parent  af60c40298a4edf8d77164fdfe2f2188470db0f7
ac from LEM in abstract ordinal

diff -r af60c40298a4 -r e06b76e5b682 OD.agda
--- a/OD.agda	Mon Aug 12 13:28:59 2019 +0900
+++ b/OD.agda	Tue Aug 13 22:21:10 2019 +0900
@@ -33,7 +33,7 @@
      eq→ : ∀ { x : Ordinal  } → def a x → def b x 
      eq← : ∀ { x : Ordinal  } → def b x → def a x 
 
-id : {n : Level} {A : Set n} → A → A
+id : {A : Set n} → A → A
 id x = x
 
 eq-refl :  {  x :  OD  } → x == x
@@ -193,13 +193,13 @@
    lemma : ps ∋ minimul ps (λ eq →  ¬p (eqo∅ eq)) 
    lemma = x∋minimul ps (λ eq →  ¬p (eqo∅ eq))
 
-∋-p : ( p : Set n ) → Dec p   -- assuming axiom of choice    
-∋-p  p with p∨¬p p
-∋-p  p | case1 x = yes x
-∋-p  p | case2 x = no x
+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 ∋-p  A                         -- assuming axiom of choice
+double-neg-eilm  {A} notnot with decp  A                         -- assuming axiom of choice
 ... | yes p = p
 ... | no ¬p = ⊥-elim ( notnot ¬p )
 
@@ -477,6 +477,53 @@
          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∋minimul 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 = IsOrdinals.TransFinite (Ordinals.isOrdinal O) {ψ} induction ox where
+                    ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
+                    ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x ))
+                    ∋-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))
+                    ∀-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 with lemma-ord (od→ord X )
+                 have_to_find | t = dont-or  t ¬¬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 )
+                        }
+         
+
 _,_ = ZF._,_ OD→ZF
 Union = ZF.Union OD→ZF
 Power = ZF.Power OD→ZF
diff -r af60c40298a4 -r e06b76e5b682 cardinal.agda
--- a/cardinal.agda	Mon Aug 12 13:28:59 2019 +0900
+++ b/cardinal.agda	Tue Aug 13 22:21:10 2019 +0900
@@ -37,6 +37,11 @@
 
 open SetProduct
 
+∋-p : (A x : OD ) → Dec ( A ∋ x ) 
+∋-p A x with p∨¬p ( A ∋ x )
+∋-p A x | case1 t = yes t
+∋-p A x | case2 t = no t
+
 _⊗_  : (A B : OD) → OD
 A ⊗ B  = record { def = λ x → SetProduct A B x }
 -- A ⊗ B  = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
@@ -48,12 +53,16 @@
 
 -- power→ :  ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
 
-func←od : { dom cod : OD } → {f : OD }  → Func dom cod ∋ f → (Ordinal → Ordinal )
+func←od : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f → (Ordinal → Ordinal )
 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma  y ) where
+   lemma1 = subst (λ k → def (Power (dom ⊗ cod)) k ) (sym {!!}) lt
    lemma : Ordinal → Ordinal
-   lemma y with IsZF.power→ isZF (dom ⊗ cod) f lt
-   lemma y | p with double-neg-eilm ( p {ord→od y} {!!} ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
-   ... | t = π2 t
+   lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) {!!} lt ) | ∋-p (ord→od f) (ord→od y)
+   lemma y | p | no n  = o∅
+   lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
+   ... | t with decp ( x  ≡ π1 t )
+   ... | yes _ = π2 t
+   ... | no _ = o∅
 
 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
 func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
@@ -80,7 +89,8 @@
        ymap : Ordinal 
        xfunc : def (Func X Y) xmap 
        yfunc : def (Func Y X) ymap 
-       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → func←od  {!!} ( func←od  {!!} y )  ≡ y
+       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) →
+          func←od {X} {Y} {xmap} xfunc ( func←od  yfunc y )  ≡ y
 
 open Onto
 
@@ -100,7 +110,7 @@
        xfunc1 = {!!}
        zfunc : def (Func Z X) zmap 
        zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od  {!!} ( func←od  zfunc z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od  xfunc1 ( func←od  zfunc z )  ≡ z
        onto-iso1   = {!!}
 
 
diff -r af60c40298a4 -r e06b76e5b682 ordinal.agda
--- a/ordinal.agda	Mon Aug 12 13:28:59 2019 +0900
+++ b/ordinal.agda	Tue Aug 13 22:21:10 2019 +0900
@@ -322,69 +322,3 @@
               dz<dz  : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x
               dz<dz refl = s<refl 
   
-  ---
-  --- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
-  ---
-  record choiced  ( X : OD) : Set (suc (suc n)) where
-   field
-      a-choice : OD
-      is-in : X ∋ a-choice
-  
-  choice-func' :  (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
-  choice-func'  X p∨¬p not = have_to_find where
-          ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
-          ψ ox = (( x : Ordinal {suc n}) → x o< ox  → ( ¬ def X x )) ∨ choiced X
-          lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
-          lemma-ord  ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where
-             ∋-p' : (A x : OD ) → Dec ( A ∋ x ) 
-             ∋-p' A x with p∨¬p ( A ∋ x )
-             ∋-p' A x | case1 t = yes t
-             ∋-p' A x | case2 t = no t
-             ∀-imply-or :  {n : Level}  {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
-                 → ((x : Ordinal {suc n}) → A x ∨ B) →  ((x : Ordinal {suc n}) → A x) ∨ B
-             ∀-imply-or {n} {A} {B} ∀AB with p∨¬p  ((x : Ordinal {suc n}) → A x)
-             ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
-             ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
-                  lemma : ¬ ((x : Ordinal {suc n}) → 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 ))
-             caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) ) 
-             caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
-             caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
-             caseΦ lx prev | no ¬p = lemma where
-                  lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
-                  lemma1 x with trio< x (ordinal lx (Φ lx))
-                  lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
-                      lemma2 : x o< (ordinal lx (Φ lx)) →  osuc x o< ordinal lx (Φ lx)
-                      lemma2 (case1 lt) = case1 lt
-                  lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
-                  lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
-                  lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
-                  lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
-                  lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
-                  lemma = ∀-imply-or lemma1
-             caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
-             caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
-             caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
-             caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
-                  lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
-                  lemma y lt with trio< y (ordinal lx x )
-                  lemma y lt | tri< a ¬b ¬c = not_found y a
-                  lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
-                  lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
-                  lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
-                  lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
-             caseOSuc lx x (case2 found) | no ¬p = case2 found
-             caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) →
-                 ψ (record { lv = lx ; ord = OSuc lx x })
-             caseOSuc1 lx x lt =  caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl))
-          have_to_find : choiced X
-          have_to_find with lemma-ord (od→ord X )
-          have_to_find | t = dont-or  t ¬¬X∋x where
-              ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (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 )
-                 }
-