Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal.agda @ 158:b97b4ee06f01
Union trans finite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 14 Jul 2019 17:26:57 +0900 |
| parents | c848550c8b39 |
| children | d16b8bf29f4f |
line wrap: on
line diff
--- a/ordinal.agda Sun Jul 14 08:04:16 2019 +0900 +++ b/ordinal.agda Sun Jul 14 17:26:57 2019 +0900 @@ -324,9 +324,9 @@ -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p -- may be we can prove this... postulate - TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } + TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) → (exists : ¬ (∀ y → ¬ ( ψ y ) )) - → {p : Set n} ( P : { y : Ordinal {n} } → ψ y → p ) + → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p ) → p -- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where