# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564629787 -32400
# Node ID 2c7d45734e3be59a06d272a07fecdbf77ab8ce10
# Parent  e59e682ad120a58eb064ee033c69f92c44606668
axiom of choice from exclusive middle done

diff -r e59e682ad120 -r 2c7d45734e3b OD.agda
--- a/OD.agda	Thu Aug 01 10:22:16 2019 +0900
+++ b/OD.agda	Thu Aug 01 12:23:07 2019 +0900
@@ -559,6 +559,9 @@
                                lx ≡ ly → ly ≡ lv (od→ord z)  → ψ z 
                           lemma6 {ly} {ox} {oy} refl refl = lemma5 (OSuc lx (ord (od→ord z)) ) (case2 s<refl)
 
+         ---
+         --- With assuption of OD is ordered,  p ∨ ( ¬ p ) <=> axiom of choice
+         ---
          record choiced {n : Level} ( X : OD {suc n}) : Set (suc (suc n)) where
             field
                 a-choice : OD {suc n}
@@ -589,9 +592,11 @@
                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 x a
-                    lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 {!!}
+                    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
@@ -610,5 +615,10 @@
                caseOSuc lx x (case2 found) | no ¬p = case2 found
             have_to_find : choiced X
             have_to_find with lemma-ord (od→ord X )
-            have_to_find | t = dont-or  t  {!!}
+            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 )
+                   }