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