Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ordinal-definable.agda @ 96:f239ffc27fd0
Power Set and L
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 08 Jun 2019 22:17:40 +0900 |
parents | f3da2c87cee0 |
children | f2b579106770 |
comparison
equal
deleted
inserted
replaced
95:f3da2c87cee0 | 96:f239ffc27fd0 |
---|---|
43 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } | 43 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y t) ; eq← = λ t → eq← x=y ( eq← y=z t) } |
44 | 44 |
45 od∅ : {n : Level} → OD {n} | 45 od∅ : {n : Level} → OD {n} |
46 od∅ {n} = record { def = λ _ → Lift n ⊥ } | 46 od∅ {n} = record { def = λ _ → Lift n ⊥ } |
47 | 47 |
48 -- OD can be iso to a subset of Ordinal | |
48 postulate | 49 postulate |
49 od→ord : {n : Level} → OD {n} → Ordinal {n} | 50 od→ord : {n : Level} → OD {n} → Ordinal {n} |
50 ord→od : {n : Level} → Ordinal {n} → OD {n} | 51 ord→od : {n : Level} → Ordinal {n} → OD {n} |
51 c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y | 52 c<→o< : {n : Level} {x y : OD {n} } → def y ( od→ord x ) → od→ord x o< od→ord y |
52 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x | 53 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → def (ord→od y) x |
245 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (subst (λ k → k o< ox ) (sym diso) (∅5 ¬p)) ) | 246 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅≡od∅ (o<→c< (subst (λ k → k o< ox ) (sym diso) (∅5 ¬p)) ) |
246 | 247 |
247 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) | 248 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
248 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) | 249 -- postulate f-extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n)) |
249 | 250 |
251 -- Power Set of X ( or constructible by λ y → def X (od→ord y ) | |
250 Def : {n : Level} → OD {suc n} → OD {suc n} | 252 Def : {n : Level} → OD {suc n} → OD {suc n} |
251 Def {n} X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def X x → def (ord→od y) x } | 253 Def {n} A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def A x } |
252 | 254 |
255 -- Constructible Set on α | |
256 L : {n : Level} → Ordinal {suc n} → OD {suc n} | |
257 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅ | |
258 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L ( record { lv = lx ; ord = ox } )) | |
259 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) | |
260 record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) } | |
261 | |
262 csuc : {n : Level} → OD {suc n} → OD {suc n} | |
263 csuc x = ord→od ( osuc ( od→ord x )) | |
264 | |
265 -- L∋ord : {n : Level} → (x : Ordinal {suc n} ) → L (osuc x) ∋ ord→od x | |
266 -- L∋ord {n} record { lv = Zero ; ord = (Φ .0) } = {!!} | |
267 -- L∋ord {n} record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } = {!!} | |
268 -- L∋ord {n} record { lv = lv ; ord = (OSuc .(lv) ord₁) } = {!!} | |
269 | |
270 -- X ⊆ OD → (P X ∩ OD ) ⊆ L (supP X) ∈ OD | |
271 | |
272 ord-of : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n} → Ordinal {suc n} | |
273 ord-of {n} A x with def A x | |
274 ... | t = x | |
275 | |
276 supP : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n} | |
277 supP A = sup-o ( ord-of A ) | |
278 | |
279 L→P : {n : Level} → (A : OD {suc n} ) → L (supP A) ∋ Def A | |
280 L→P {n} A = {!!} | |
253 | 281 |
254 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 282 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
255 OD→ZF {n} = record { | 283 OD→ZF {n} = record { |
256 ZFSet = OD {suc n} | 284 ZFSet = OD {suc n} |
257 ; _∋_ = _∋_ | 285 ; _∋_ = _∋_ |
273 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) } | 301 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) } |
274 Union : OD {suc n} → OD {suc n} | 302 Union : OD {suc n} → OD {suc n} |
275 Union U = record { def = λ y → osuc y o< (od→ord U) } | 303 Union U = record { def = λ y → osuc y o< (od→ord U) } |
276 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) | 304 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) |
277 Power : OD {suc n} → OD {suc n} | 305 Power : OD {suc n} → OD {suc n} |
278 Power X = record { def = λ y → ∀ (x : Ordinal {suc n} ) → def (ord→od y) x → def X x } | 306 Power A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def A x } |
279 ZFSet = OD {suc n} | 307 ZFSet = OD {suc n} |
280 _∈_ : ( A B : ZFSet ) → Set (suc n) | 308 _∈_ : ( A B : ZFSet ) → Set (suc n) |
281 A ∈ B = B ∋ A | 309 A ∈ B = B ∋ A |
282 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) | 310 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) |
283 _⊆_ A B {x} = A ∋ x → B ∋ x | 311 _⊆_ A B {x} = A ∋ x → B ∋ x |
284 _∩_ : ( A B : ZFSet ) → ZFSet | 312 -- _∩_ : ( A B : ZFSet ) → ZFSet |
285 A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) | 313 -- A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) |
286 _∪_ : ( A B : ZFSet ) → ZFSet | 314 -- _∪_ : ( A B : ZFSet ) → ZFSet |
287 A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) ) | 315 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) ) |
288 infixr 200 _∈_ | 316 infixr 200 _∈_ |
289 infixr 230 _∩_ _∪_ | 317 -- infixr 230 _∩_ _∪_ |
290 infixr 220 _⊆_ | 318 infixr 220 _⊆_ |
291 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} )) | 319 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} )) |
292 isZF = record { | 320 isZF = record { |
293 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } | 321 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } |
294 ; pair = pair | 322 ; pair = pair |
313 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) | 341 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) |
314 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) | 342 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) |
315 empty x () | 343 empty x () |
316 --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def X x } | 344 --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def X x } |
317 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x | 345 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x |
318 power→ A t P∋t {x} t∋x = {!!} | 346 power→ A t P∋t {x} t∋x = P∋t (od→ord x) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) |
319 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t | 347 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t |
320 power← A t t→A z _ = {!!} | 348 power← A t t→A z _ = {!!} |
321 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} | 349 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} |
322 union-u X z U>z = ord→od ( osuc ( od→ord z ) ) | 350 union-u X z U>z = ord→od ( osuc ( od→ord z ) ) |
323 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z | 351 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z |