diff OD.agda @ 188:1f2c8b094908

axiom of choice → p ∨ ¬ p
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 25 Jul 2019 13:11:21 +0900
parents ac872f6b8692
children 540b845ea2de
line wrap: on
line diff
--- a/OD.agda	Tue Jul 23 11:08:24 2019 +0900
+++ b/OD.agda	Thu Jul 25 13:11:21 2019 +0900
@@ -191,6 +191,22 @@
 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
 
+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
+   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))
+
 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
@@ -458,6 +474,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}
+
          -- another form of regularity 
          --
          ε-induction : {n m : Level} { ψ : OD {suc n} → Set m}