# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1564033339 -32400
# Node ID 540b845ea2de0db2b7b8df99cd94898212437715
# Parent  1f2c8b09490892468e6dfa6697cf0b06a8bfbe65
Axiom of choies implies p ∨ ( ¬ p )

diff -r 1f2c8b094908 -r 540b845ea2de OD.agda
--- a/OD.agda	Thu Jul 25 13:11:21 2019 +0900
+++ b/OD.agda	Thu Jul 25 14:42:19 2019 +0900
@@ -194,19 +194,35 @@
 ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p
 ppp {n} {p} {a} d = d
 
-p∨¬p : { n : Level } → { p : Set (suc n) } → p ∨ ( ¬ p )
-p∨¬p {n} {p} with record { def = λ x → p } | record { def = λ x → ¬ p }  
-... | ps | ¬ps with is-o∅ ( od→ord ps)
-p∨¬p {n} {p} | ps | ¬ps | yes eq = case2 (¬p eq) where
-   ¬p : {ps1 : Ordinal {suc n}} → ( ps1  ≡ o∅ {suc n} ) → p → ⊥
-   ¬p refl = {!!}
-p∨¬p {n} {p} | ps | ¬ps | no ¬p = case1 (ppp {n} {p} {minimul ps (λ eq →  ¬p (eqo∅ eq))} (
-       def-subst {suc n} {ps} {_} {record { def = λ x → p }} {od→ord (minimul ps (λ eq →  ¬p (eqo∅ eq)))} lemma {!!} refl )) where
+--
+-- Axiom of choice in intutionistic logic implies the exclude middle
+--     https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
+--
+p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )
+p∨¬p {n} p with is-o∅ ( od→ord ( record { def = λ x → p } ))
+p∨¬p {n} p | yes eq = case2 (¬p eq) where
+   ps = record { def = λ x → p }
+   lemma : ps == od∅ → p → ⊥
+   lemma eq p0 = ¬x<0 {n} {od→ord ps} (eq→ eq p0 )
+   ¬p : (od→ord ps ≡ o∅) → p → ⊥
+   ¬p eq = lemma ( subst₂ (λ j k → j ==  k ) oiso o∅≡od∅ ( o≡→== eq ))
+p∨¬p {n} p | no ¬p = case1 (ppp {n} {p} {minimul ps (λ eq →  ¬p (eqo∅ eq))} lemma) where
+   ps = record { def = λ x → p }
    eqo∅ : ps ==  od∅ {suc n} → od→ord ps ≡  o∅ {suc n} 
    eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) 
    lemma : ps ∋ minimul ps (λ eq →  ¬p (eqo∅ eq)) 
    lemma = x∋minimul ps (λ eq →  ¬p (eqo∅ eq))
 
+∋-p : { n : Level } → ( p : Set (suc n) ) → Dec p 
+∋-p {n} p with p∨¬p p
+∋-p {n} p | case1 x = yes x
+∋-p {n} p | case2 x = no x
+
+double-neg-eilm : {n  : Level } {A : Set (suc n)} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
+double-neg-eilm {n} {A} notnot with ∋-p  A
+... | yes p = p
+... | no ¬p = ⊥-elim ( notnot ¬p )
+
 OrdP : {n : Level} →  ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y )
 OrdP {n} x y with trio< x (od→ord y)
 OrdP {n} x y | tri< a ¬b ¬c = no ¬c
@@ -386,7 +402,6 @@
               lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
               lemma = sup-o<   
 
-         -- double-neg-eilm : {n  : Level } {A : Set n} → ¬ ¬ A → A      -- we don't have this in intutionistic logic
          -- 
          -- Every set in OD is a subset of Ordinals
          -- 
@@ -474,8 +489,8 @@
          choice : (X : OD {suc n} ) → {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
 
-         -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD {suc n}
-
+         -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) )  → ¬ ( X == od∅ ) → OD {suc n}
+         --
          -- another form of regularity 
          --
          ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}