### changeset 210:2c7d45734e3b

axiom of choice from exclusive middle done
author Shinji KONO Thu, 01 Aug 2019 12:23:07 +0900 e59e682ad120 6bb5d57c9561 0a1804cc9d0a OD.agda 1 files changed, 13 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
```--- 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 )
+                   }
```