Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 137:c7c9f3efc428
replace using Select
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Jul 2019 08:56:25 +0900 |
| parents | 3cc848664a86 |
| children | 567084f2278f |
| files | HOD.agda |
| diffstat | 1 files changed, 2 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/HOD.agda Sun Jul 07 02:19:32 2019 +0900 +++ b/HOD.agda Sun Jul 07 08:56:25 2019 +0900 @@ -308,6 +308,8 @@ lemma : {x : Ordinal} → ¬ ((y : Ordinal) → ¬ def X y ∧ (x ≡ od→ord (ψ (Ord y)))) → {y : Ordinal} → y o< x → ¬ ((y₁ : Ordinal) → ¬ def X y₁ ∧ (y ≡ od→ord (ψ (Ord y₁)))) lemma {x} notx {y} y<x noty = notx ( λ z prod → noty z ( record { proj1 = proj1 prod ; proj2 = {!!} } )) + Replace' : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n} + Replace' X ψ = Select ( Ord (sup-o ( λ x → od→ord (ψ (ord→od x ))))) ( λ x → ¬ (∀ (y : Ordinal ) → ¬ ( def X y ∧ ( x == ψ (Ord y) )))) Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n} Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x ; otrans = lemma } where