Mercurial > hg > Members > kono > Proof > ZF-in-agda
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}