Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 132:327d49c2478b
use OD for replace condition
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 06 Jul 2019 18:31:46 +0900 |
| parents | 5dcd5a3583a0 |
| children | 35ce91192cf4 |
| files | ordinal-definable.agda zf.agda |
| diffstat | 2 files changed, 7 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/ordinal-definable.agda Wed Jul 03 00:25:58 2019 +0900 +++ b/ordinal-definable.agda Sat Jul 06 18:31:46 2019 +0900 @@ -278,6 +278,9 @@ csuc : {n : Level} → OD {suc n} → OD {suc n} csuc x = Ord ( osuc ( od→ord x )) +f-rel : {n : Level} → (X : OD {suc n} ) → ( ψ : OD {suc n} → OD {suc n} ) → OD {suc n} +f-rel {n} X ψ = record { def = λ x → ¬ ( (y : Ordinal {suc n}) → def X y → ¬ ( x ≡ od→ord (ψ (Ord y )))) } + -- Power Set of X ( or constructible by λ y → def X (od→ord y ) ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n} @@ -314,7 +317,7 @@ _∩_ : ( A B : OD ) → OD A ∩ B = record { def = λ x → def A x ∧ def B x } Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} - Replace X ψ = record { def = λ x → x o< sup-o ( λ x → od→ord (ψ (X ∩ (ord→od x )))) } + Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (X ∩ (ord→od x ))))) ∧ def (f-rel X ψ) x } Union : OD {suc n} → OD {suc n} Union U = record { def = λ y → osuc y o< (od→ord U) } -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) @@ -346,8 +349,6 @@ ; infinity∅ = infinity∅ ; infinity = λ _ → infinity ; selection = λ {X} {ψ} {y} → selection {ψ} {X} {y} - ; repl-x = repl-x - ; repl-x-∈ = repl-x-∈ ; replacement← = replacement← ; replacement→ = replacement→ } where @@ -414,18 +415,9 @@ } where lemma : (cond : ((y : OD) → X ∋ y → ψ y ) ∧ (X ∋ y) ) → ψ y lemma cond = (proj1 cond) y (proj2 cond) - repl-x : {ψ : OD → OD} {X x : OD} → (lt : Replace X ψ ∋ x) → OD - repl-x {ψ} {X} {x} lt = Ord (sup-x (λ x → od→ord (ψ (ord→od x)))) - repl-x-∈ : {ψ : OD → OD} {X x : OD} → (lt : Replace X ψ ∋ x) → X ∋ repl-x {ψ} {X} {x} lt - repl-x-∈ {ψ} {X} {x} lt = {!!} - X∩x : {X x : OD} → X ∋ x → X ∩ x ≡ x - X∩x = {!!} replacement← : {ψ : OD → OD} (X x : OD) → X ∋ x → Replace X ψ ∋ ψ x - replacement← {ψ} X x lt = def-subst ( sup-c< ψ {x} ) (sym lemma) refl where - lemma : record { def = λ x → x o< sup-o ( λ x → od→ord (ψ (X ∩ (ord→od x )))) } ≡ - record { def = λ x → x o< sup-o ( λ x → od→ord (ψ (ord→od x ))) } - lemma = {!!} - replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → x == ψ (repl-x {ψ} {X} {x} lt) + replacement← {ψ} X x lt = record { proj1 = sup-o< {suc n} {λ x → od→ord (ψ (ord→od x)) } ; proj2 = {!!} } + replacement→ : {ψ : OD → OD} (X x : OD) → (lt : Replace X ψ ∋ x) → {y : OD} → ¬ (¬ (ψ x == y)) replacement→ {ψ} X x = {!!} ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
--- a/zf.agda Wed Jul 03 00:25:58 2019 +0900 +++ b/zf.agda Sat Jul 06 18:31:46 2019 +0900 @@ -77,10 +77,8 @@ infinity : ∀( X x : ZFSet ) → x ∈ infinite → ( x ∪ ｛ x ｝) ∈ infinite selection : ∀ { X : ZFSet } → { ψ : (x : ZFSet ) → Set m } → ∀ { y : ZFSet } → (((y : ZFSet) → y ∈ X → ψ y ) ∧ ( y ∈ X ) ) ⇔ (y ∈ Select X ψ ) -- replacement : ∀ x ∀ y ∀ z ( ( ψ ( x , y ) ∧ ψ ( x , z ) ) → y = z ) → ∀ X ∃ A ∀ y ( y ∈ A ↔ ∃ x ∈ X ψ ( x , y ) ) - repl-x : {ψ : ZFSet → ZFSet} → { X x : ZFSet } ( lt : x ∈ Replace X ψ ) → ZFSet - repl-x-∈ : {ψ : ZFSet → ZFSet} → { X x : ZFSet } → (lt : x ∈ Replace X ψ ) → repl-x lt ∈ X replacement← : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → x ∈ X → ψ x ∈ Replace X ψ - replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → x ≈ ψ ( repl-x lt ) + replacement→ : {ψ : ZFSet → ZFSet} → ∀ ( X x : ZFSet ) → ( lt : x ∈ Replace X ψ ) → ∀ {y : ZFSet} → ¬ ( ¬ ( ψ x ≈ y ) ) -- -- ∀ z [ ∀ x ( x ∈ z → ¬ ( x ≈ ∅ ) ) ∧ ∀ x ∀ y ( x , y ∈ z ∧ ¬ ( x ≈ y ) → x ∩ y ≈ ∅ ) → ∃ u ∀ x ( x ∈ z → ∃ t ( u ∩ x) ≈ ｛ t ｝) ] -- axiom-of-choice : Set (suc n) -- axiom-of-choice = ?