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

comparison ordinal.agda @ 158:b97b4ee06f01

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
comparison
equal deleted inserted replaced
157:afc030b7c8d0 158:b97b4ee06f01
322 caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox }) 322 caseOSuc lx ox (TransFinite caseΦ caseOSuc record { lv = lx ; ord = ox })
323 323
324 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p 324 -- (¬ (∀ y → ¬ ( ψ y ))) → (ψ y → p ) → p
325 -- may be we can prove this... 325 -- may be we can prove this...
326 postulate 326 postulate
327 TransFiniteExists : {n : Level} → { ψ : Ordinal {n} → Set n } 327 TransFiniteExists : {n m l : Level} → ( ψ : Ordinal {n} → Set m )
328 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 328 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
329 → {p : Set n} ( P : { y : Ordinal {n} } → ψ y → p ) 329 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → p )
330 → p 330 → p
331 331
332 -- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where 332 -- TransFiniteExists {n} {ψ} exists {p} P = ⊥-elim ( exists lemma ) where
333 -- lemma : (y : Ordinal {n} ) → ¬ ψ y 333 -- lemma : (y : Ordinal {n} ) → ¬ ψ y
334 -- lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy 334 -- lemma y ψy = ( TransFinite {n} {{!!}} {!!} {!!} y ) ψy