Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 142:c30bc9f5bd0d
Power Set
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 08 Jul 2019 12:13:19 +0900 |
| parents | 2a5519dcc167 |
| children | 3ba37037faf4 |
line wrap: on
line diff
--- a/ordinal.agda Mon Jul 08 00:20:30 2019 +0900 +++ b/ordinal.agda Mon Jul 08 12:13:19 2019 +0900 @@ -313,3 +313,12 @@ TransFinite caseΦ caseOSuc record { lv = lx ; ord = (OSuc lx ox) } = caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox }) +-- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p +TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } + → (exists : ¬ (∀ y → ¬ ( ψ y ) )) + → {p : Set n} ( P : { y : Ordinal {n} } → ψ y → p ) + → p +TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where + lemma : (y : Ordinal {n} ) → ¬ ψ y + lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy +