Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff ordinal-definable.agda @ 77:75ba8cf64707
Power Set on going ...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 02 Jun 2019 15:12:26 +0900 |
parents | 8e8f54e7a030 |
children | 9a7a64b2388c |
line wrap: on
line diff
--- a/ordinal-definable.agda Sun Jun 02 11:56:43 2019 +0900 +++ b/ordinal-definable.agda Sun Jun 02 15:12:26 2019 +0900 @@ -283,15 +283,6 @@ lemma o∅ ne | yes refl | () lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p)) --- ∃-set : {n : Level} → ( x : OD {suc n} ) → ( ψ : OD {suc n} → Set (suc n) ) → Set (suc n) --- ∃-set = {!!} - --- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc (suc n)) (suc (suc n )) - --- ==∅→≡ : {n : Level} → { x : OD {suc n} } → ( x == od∅ {suc n} ) → x ≡ od∅ {suc n} --- ==∅→≡ {n} {x} eq = cong ( λ k → record { def = k } ) (trans {!!} ∅-base-def ) where - - open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} @@ -316,8 +307,9 @@ x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) } 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 ) Power : OD {suc n} → OD {suc n} - Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y ) } + Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) } ZFSet = OD {suc n} _∈_ : ( A B : ZFSet ) → Set (suc n) A ∈ B = B ∋ A @@ -355,16 +347,14 @@ proj2 (pair A B ) = case2 refl empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) empty x () - -- Power x = record { def = λ y → (z : Ordinal {suc n} ) → ( def x y ∧ def (ord→od z) y ) } + --- Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → ( def X x ∧ def (ord→od y) x ) } power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x - power→ A t P∋t {x} t∋x = transitive {n} {A} {t} {x} lemma t∋x where - lemma : A ∋ t - lemma = proj1 (P∋t (od→ord x )) - power← : (A t : OD) {x : OD} → (t ∋ x → A ∋ x) → Power A ∋ t - power← A t {x} t→A y = record { proj1 = lemma1 ; proj2 = lemma2 } where - lemma1 : def A (od→ord t) + power→ A t P∋t {x} t∋x = proj1 (P∋t (od→ord x) ) + power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t + power← A t t→A z = record { proj1 = lemma2 ; proj2 = lemma1 } where + lemma1 : def (ord→od (od→ord t)) z lemma1 = {!!} - lemma2 : def (ord→od y) (od→ord t) + lemma2 : def A z lemma2 = {!!} union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} union-u X z U>z = ord→od ( osuc ( od→ord z ) )