Mercurial > hg > Members > kono > Proof > ZF-in-agda

diff ordinal.agda @ 165:d16b8bf29f4f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minor fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 16 Jul 2019 09:57:01 +0900
parents b97b4ee06f01
children ea0e7927637a
line wrap: on
line diff
--- a/ordinal.agda	Mon Jul 15 19:10:08 2019 +0900
+++ b/ordinal.agda	Tue Jul 16 09:57:01 2019 +0900
@@ -332,4 +332,10 @@
 -- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where
 --     lemma : (y : Ordinal {n} ) → ¬ ψ y
 --     lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy
+TransFiniteExists' : {n m l : Level} → ( ψ : Ordinal {n} → Set m ) 
+  → {p : Set l} ( P : { y : Ordinal {n} } →  ψ y → ¬ p )
+  → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
+  → ¬ p
+TransFiniteExists' {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 
+