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

comparison ordinal-definable.agda @ 97:f2b579106770

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
power set using sup on Def
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 09 Jun 2019 19:41:53 +0900
parents f239ffc27fd0
children 1ff0ddc991ac
comparison
equal deleted inserted replaced
96:f239ffc27fd0 97:f2b579106770
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 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)) )
247 247
248 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 248 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
249 -- 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))
250 250
251 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
252 Def : {n : Level} → OD {suc n} → OD {suc n}
253 Def {n} A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def A x }
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} 251 csuc : {n : Level} → OD {suc n} → OD {suc n}
263 csuc x = ord→od ( osuc ( od→ord x )) 252 csuc x = ord→od ( osuc ( od→ord x ))
253
254 -- Power Set of X ( or constructible by λ y → def X (od→ord y )
255
256 ZFSubset : {n : Level} → (A x : OD {suc n} ) → OD {suc n}
257 ZFSubset A x = record { def = λ y → def A y ∧ def x y }
258
259 Def : {n : Level} → (A : OD {suc n}) → OD {suc n}
260 Def {n} A = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
261
262 -- Constructible Set on α
263 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
264 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅
265 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) )
266 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
267 record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) }
264 268
265 -- L∋ord : {n : Level} → (x : Ordinal {suc n} ) → L (osuc x) ∋ ord→od x 269 -- L∋ord : {n : Level} → (x : Ordinal {suc n} ) → L (osuc x) ∋ ord→od x
266 -- L∋ord {n} record { lv = Zero ; ord = (Φ .0) } = {!!} 270 -- L∋ord {n} record { lv = Zero ; ord = (Φ .0) } = {!!}
267 -- L∋ord {n} record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } = {!!} 271 -- L∋ord {n} record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } = {!!}
268 -- L∋ord {n} record { lv = lv ; ord = (OSuc .(lv) ord₁) } = {!!} 272 -- L∋ord {n} record { lv = lv ; ord = (OSuc .(lv) ord₁) } = {!!}
274 ... | t = x 278 ... | t = x
275 279
276 supP : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n} 280 supP : {n : Level} → (A : OD {suc n} ) → Ordinal {suc n}
277 supP A = sup-o ( ord-of A ) 281 supP A = sup-o ( ord-of A )
278 282
279 L→P : {n : Level} → (A : OD {suc n} ) → L (supP A) ∋ Def A 283 L→P : {n : Level} → (A x : OD {suc n} ) → L {n} (supP A) ∋ ZFSubset A x
280 L→P {n} A = {!!} 284 L→P {n} A x with sup-o< (ord-of A) {{!!}}
285 ... | lt = {!!}
281 286
282 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 287 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
283 OD→ZF {n} = record { 288 OD→ZF {n} = record {
284 ZFSet = OD {suc n} 289 ZFSet = OD {suc n}
285 ; _∋_ = _∋_ 290 ; _∋_ = _∋_
301 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) } 306 x , y = record { def = λ z → z o< (omax (od→ord x) (od→ord y)) }
302 Union : OD {suc n} → OD {suc n} 307 Union : OD {suc n} → OD {suc n}
303 Union U = record { def = λ y → osuc y o< (od→ord U) } 308 Union U = record { def = λ y → osuc y o< (od→ord U) }
304 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 309 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
305 Power : OD {suc n} → OD {suc n} 310 Power : OD {suc n} → OD {suc n}
306 Power A = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def A x } 311 Power A = Def A
307 ZFSet = OD {suc n} 312 ZFSet = OD {suc n}
308 _∈_ : ( A B : ZFSet ) → Set (suc n) 313 _∈_ : ( A B : ZFSet ) → Set (suc n)
309 A ∈ B = B ∋ A 314 A ∈ B = B ∋ A
310 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 315 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
311 _⊆_ A B {x} = A ∋ x → B ∋ x 316 _⊆_ A B {x} = A ∋ x → B ∋ x
318 infixr 220 _⊆_ 323 infixr 220 _⊆_
319 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} )) 324 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
320 isZF = record { 325 isZF = record {
321 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 326 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
322 ; pair = pair 327 ; pair = pair
323 ; union-u = union-u 328 ; union-u = λ _ z _ → csuc z
324 ; union→ = union→ 329 ; union→ = union→
325 ; union← = union← 330 ; union← = union←
326 ; empty = empty 331 ; empty = empty
327 ; power→ = power→ 332 ; power→ = power→
328 ; power← = power← 333 ; power← = power←
339 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 344 pair : (A B : OD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
340 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) 345 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
341 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) 346 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
342 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 347 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
343 empty x () 348 empty x ()
344 --- Power X = record { def = λ t → ∀ (x : Ordinal {suc n} ) → def (ord→od t) x → def X x } 349 --- ZFSubset A x = record { def = λ y → def A y ∧ def x y }
350 --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )
345 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ x 351 power→ : (A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → A ∋ 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 ) 352 power→ A t P∋t {x} t∋x = proj1 lemma-s where
353 lemma-t : ZFSubset A {!!} ∋ csuc t
354 lemma-t = record { proj1 = {!!} ; proj2 = {!!} }
355 lemma-s : ZFSubset A {!!} ∋ x
356 lemma-s = {!!} -- transitive {!!} t∋x
357 lemma : od→ord (ZFSubset A (ord→od (od→ord (csuc t))) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
358 lemma = sup-o< {suc n} ( λ x → od→ord ( ZFSubset A (ord→od x )))
347 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t 359 power← : (A t : OD) → ({x : OD} → (t ∋ x → A ∋ x)) → Power A ∋ t
348 power← A t t→A z _ = {!!} 360 power← A t t→A = {!!} where
349 union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n} 361 lemma-eq : ZFSubset A t == t
350 union-u X z U>z = ord→od ( osuc ( od→ord z ) ) 362 eq→ lemma-eq {z} w = proj2 w
351 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z ∋ z 363 eq← lemma-eq {z} w = record { proj2 = w ;
364 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
365 lemma : od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
366 lemma = sup-o< {suc n} ( λ x → od→ord ( ZFSubset A (ord→od x )))
367 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z
352 union-lemma-u {X} {z} U>z = lemma <-osuc where 368 union-lemma-u {X} {z} U>z = lemma <-osuc where
353 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz 369 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
354 lemma {oz} {ooz} lt = def-subst {suc n} {ord→od ooz} (o<→c< lt) refl refl 370 lemma {oz} {ooz} lt = def-subst {suc n} {ord→od ooz} (o<→c< lt) refl refl
355 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 371 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
356 union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y )) 372 union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
358 union→ X y u xx | tri< a ¬b ¬c | () 374 union→ X y u xx | tri< a ¬b ¬c | ()
359 union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where 375 union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where
360 lemma : {oX ou ooy : Ordinal {suc n}} → ou ≡ ooy → ou o< oX → ooy o< oX 376 lemma : {oX ou ooy : Ordinal {suc n}} → ou ≡ ooy → ou o< oX → ooy o< oX
361 lemma refl lt = lt 377 lemma refl lt = lt
362 union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 378 union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx ))
363 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z ) 379 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z )
364 union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (union-u X z X∋z)} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z } 380 union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} (o<→c< X∋z) oiso (sym diso) ; proj2 = union-lemma-u X∋z }
365 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y 381 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
366 ψiso {ψ} t refl = t 382 ψiso {ψ} t refl = t
367 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 383 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
368 selection {ψ} {X} {y} = record { 384 selection {ψ} {X} {y} = record {
369 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) } 385 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = ψiso {ψ} (proj2 cond) (sym oiso) }