Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
| 187:ac872f6b8692 | 188:1f2c8b094908 |
|---|---|
| 188 | 188 |
| 189 is-o∅ : {n : Level} → ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} ) | 189 is-o∅ : {n : Level} → ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} ) |
| 190 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl | 190 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl |
| 191 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () ) | 191 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () ) |
| 192 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) | 192 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) |
| 193 | |
| 194 ppp : { n : Level } → { p : Set (suc n) } { a : OD {suc n} } → record { def = λ x → p } ∋ a → p | |
| 195 ppp {n} {p} {a} d = d | |
| 196 | |
| 197 p∨¬p : { n : Level } → { p : Set (suc n) } → p ∨ ( ¬ p ) | |
| 198 p∨¬p {n} {p} with record { def = λ x → p } | record { def = λ x → ¬ p } | |
| 199 ... | ps | ¬ps with is-o∅ ( od→ord ps) | |
| 200 p∨¬p {n} {p} | ps | ¬ps | yes eq = case2 (¬p eq) where | |
| 201 ¬p : {ps1 : Ordinal {suc n}} → ( ps1 ≡ o∅ {suc n} ) → p → ⊥ | |
| 202 ¬p refl = {!!} | |
| 203 p∨¬p {n} {p} | ps | ¬ps | no ¬p = case1 (ppp {n} {p} {minimul ps (λ eq → ¬p (eqo∅ eq))} ( | |
| 204 def-subst {suc n} {ps} {_} {record { def = λ x → p }} {od→ord (minimul ps (λ eq → ¬p (eqo∅ eq)))} lemma {!!} refl )) where | |
| 205 eqo∅ : ps == od∅ {suc n} → od→ord ps ≡ o∅ {suc n} | |
| 206 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq)) | |
| 207 lemma : ps ∋ minimul ps (λ eq → ¬p (eqo∅ eq)) | |
| 208 lemma = x∋minimul ps (λ eq → ¬p (eqo∅ eq)) | |
| 193 | 209 |
| 194 OrdP : {n : Level} → ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y ) | 210 OrdP : {n : Level} → ( x : Ordinal {suc n} ) ( y : OD {suc n} ) → Dec ( Ord x ∋ y ) |
| 195 OrdP {n} x y with trio< x (od→ord y) | 211 OrdP {n} x y with trio< x (od→ord y) |
| 196 OrdP {n} x y | tri< a ¬b ¬c = no ¬c | 212 OrdP {n} x y | tri< a ¬b ¬c = no ¬c |
| 197 OrdP {n} x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) | 213 OrdP {n} x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl ) |
| 455 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] | 471 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ] |
| 456 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 472 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
| 457 choice-func X {x} not X∋x = minimul x not | 473 choice-func X {x} not X∋x = minimul x not |
| 458 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 474 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
| 459 choice X {A} X∋A not = x∋minimul A not | 475 choice X {A} X∋A not = x∋minimul A not |
| 476 | |
| 477 -- choice-func' : (X : OD {suc n} ) → (∋-p : (A x : OD {suc n} ) → Dec ( A ∋ x ) ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD {suc n} | |
| 460 | 478 |
| 461 -- another form of regularity | 479 -- another form of regularity |
| 462 -- | 480 -- |
| 463 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | 481 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} |
| 464 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | 482 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) |